Semantically guiding a first-order theorem prover with a soft model
Date
2004
Authors
Binas, Arnold
Slaney, John K
Journal Title
Journal ISSN
Volume Title
Publisher
AAAI Press
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.
Description
Keywords
Citation
Collections
Source
Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence
Type
Conference paper