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.
| Original language | English |
|---|---|
| Pages | 948-949 |
| Number of pages | 2 |
| Publication status | Published - 2004 |
| Event | Proceedings - Nineteenth National Conference on Artificial Intelligence (AAAI-2004): Sixteenth Innovative Applications of Artificial Intelligence Conference (IAAI-2004) - San Jose, CA, United States Duration: 25 Jul 2004 → 29 Jul 2004 |
Conference
| Conference | Proceedings - Nineteenth National Conference on Artificial Intelligence (AAAI-2004): Sixteenth Innovative Applications of Artificial Intelligence Conference (IAAI-2004) |
|---|---|
| Country/Territory | United States |
| City | San Jose, CA |
| Period | 25/07/04 → 29/07/04 |