Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

11

IANDC
1998

favoriteEmaildiscussreport

72views more IANDC 1998»

On the Modelling of Search in Theorem Proving - Towards a Theory of Strategy Analysis

13 years 4 months ago

On the Modelling of Search in Theorem Proving - Towards a Theory of Strategy Analysis

Download profs.sci.univr.it

We present a model for representing search in theorem proving. This model captures the notion of contraction, which has been central in some of the recent developments in theorem proving. We outline an approach to measuring the complexity of search which can be applied to analyze and evaluate the behaviour of theorem-proving strategies. Using our framework, we compare contraction-based strategies of diﬀerent contraction power and show how they aﬀect the evolution of the respective search spaces during the derivation.

Maria Paola Bonacina, Jieh Hsiang

Real-time Traffic

Diﬀerent Contraction Power | IANDC 1998 | Model | Respective Search Spaces |

claim paper

Related Content

» A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering

» Formally Analyzing Expected Time Complexity of Algorithms Using Theorem Proving

» The Game of Hex An Automatic Theorem Proving Approach to Game Programming

» HigherOrder Coloured Unification and Natural Language Semantics

» Bounded Relational Analysis of Free Data Types

» Ordered Semantic Hyper Linking

» Reasoning by Symmetry and Function Ordering in Finite Model Generation

» Probabilistic Model Checking Modulo Theories

» Integrating parallel interactions into cooperative search

» Computing minimum cuts by randomized search heuristics

Post Info
More Details (n/a)

Added	22 Dec 2010
Updated	22 Dec 2010
Type	Journal
Year	1998
Where	IANDC
Authors	Maria Paola Bonacina, Jieh Hsiang

Comments (0)