Name
Abstract | ||
|---|---|---|
SOLAR (SOL for Advanced Reasoning) is a first-order clausal consequence finding system based on the SOL (Skip Ordered Linear) tableau calculus. The ability to find non-trivial consequences of an axiom set is useful in many applications of Artificial Intelligence such as theorem proving, query answering and nonmonotonic reasoning. SOL is a connection tableau calculus which is complete for finding the non-subsumed consequences of a clausal theory. SOLAR is an efficient implementation of SOL that employs several methods to prune away redundant branches of the search space. This paper introduces some of the key pruning and control strategies implemented in SOLAR and demonstrates their effectiveness on a collection of benchmark problems. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.3233/AIC-2010-0465 | AI Commun. |
Keywords | Field | DocType |
advanced reasoning,first-order clausal consequence,connection tableau calculus,artificial intelligence,skip ordered linear,tableau calculus,automated deduction system,benchmark problem,consequence finding,clausal theory,control strategy,axiom set,automated deduction | Computer science,Axiom,Automated theorem proving,First-order logic,Non-monotonic logic,Artificial intelligence,Applications of artificial intelligence | Journal |
Volume | Issue | ISSN |
23 | 2-3 | 0921-7126 |
Citations | PageRank | References |
23 | 1.10 | 20 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hidetomo Nabeshima | 1 | 154 | 14.88 |
| Koji Iwanuma | 2 | 138 | 17.65 |
| Katsumi Inoue | 3 | 1271 | 112.78 |
| Oliver Ray | 4 | 171 | 13.02 |