Semantically Guiding a First-Order Theorem Prover with a Soft Model

Various versions of our first-order logic theorem prover SCOTT have been developed over the past decade to employ the concept of semantic guidance for improving the underlying system OTTER by McCune. We introduce our latest attempt to speed up OTTER’s proof search, Softie. While the various SCOTTs consulted an ordinary constraint solver to gain information about the problem to be solved, Softie is implemented from scratch and uses a solver capable of handling soft constraints.

Authors

• Arnold Binas
• John Slaney Abdul Sattar

Keywords

No keywords are indexed for this paper.