Semantically guiding a first-order theorem prover with a soft model

Abstract

The latest version, Softie, of the first order theorem prover, OTTER with a soft model is developed. The new system is developed to speed up the employment of the semantic guidance concept for improving OTTER's proof search. The first order theorem prover OTTER searches for refutation proofs by means of the given clause algorithm, which partitions the clauses of a problem into the usable list (UL). Softie is built from scratch and maintains a single and large soft model of almost the whole current UL. The new Softie uses a guiding model which is generated by SFINDER, a version of FINDER that handle soft constraints. Show more