Sciweavers

Share
ECAI
2004
Springer

Guiding a Theorem Prover with Soft Constraints

11 years 4 months ago
Guiding a Theorem Prover with Soft Constraints
Attempts to use finite models to guide the search for proofs by resolution and the like in first order logic all suffer from the need to trade off the expense of generating and maintaining models against the improvement in quality of guidance as investment in the semantic aspect of the reasoning is increased. Previous attempts to resolve this tradeoff have resulted either in poor selection of models, or in fragility as the search becomes over-sensitive to the order of clauses, or in extreme slowness. Here we present a fresh approach, whereby most of the clauses for which a model is sought are treated as soft constraints. The result is a partial model of all the clauses rather than an exact model of only a subset of them. This allows our system to combine the speed of maintaining just a single model with the robustness previously requiring multiple models. We present experimental evidence of benefits over a range of first order problem domains. 1 THE PROBLEM: INTELLIGENT PROOF SEARC...
John K. Slaney, Arnold Binas, David Price
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where ECAI
Authors John K. Slaney, Arnold Binas, David Price
Comments (0)
books