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

Arnold Binas and John Slaney

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.