TY - JOUR
T1 - SOLAR: An automated deduction system for consequence finding
AU - Nabeshima, Hidetomo
AU - Iwanuma, Koji
AU - Inoue, Katsumi
AU - Ray, Oliver
N1 - Other identifier: 2001174
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?eid=2-s2.0-77950226288&partnerID=8YFLogxK
U2 - 10.3233/AIC-2010-0465
DO - 10.3233/AIC-2010-0465
M3 - Article
VL - 23
JO - AI Communications
JF - AI Communications
SN - 0921-7126
IS - 2-3
M1 - 183-203
ER -