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

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 19

Student Abstracts

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.