Skip navigation
Skip navigation

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

Binas, Arnold; Slaney, John K


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...[Show more]

CollectionsANU Research Publications
Date published: 2004
Type: Conference paper
Source: Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence


There are no files associated with this item.

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator