ECAI 2004 Conference Paper

[PDF] [full paper] [prev] [tofc] [next]

Guiding a Theorem Prover with Soft Constraints

John Slaney, Arnold Binas, David Price

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 degradation in quality of guidance as investment in the semantic aspect of the reasoning is decreased. 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 wide range of first order problems domains.

Keywords: automated reasoning, theorem proving

Citation: John Slaney, Arnold Binas, David Price: Guiding a Theorem Prover with Soft Constraints. In R.López de Mántaras and L.Saitta (eds.): ECAI2004, Proceedings of the 16th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2004, pp.221-225.

[prev] [tofc] [next]

ECAI-2004 is organised by the European Coordinating Committee for Artificial Intelligence (ECCAI) and hosted by the Universitat Politècnica de València on behalf of Asociación Española de Inteligencia Artificial (AEPIA) and Associació Catalana d'Intel-ligència Artificial (ACIA).