Skip to content

SOLAR: An automated deduction system for consequence finding

Research output: Contribution to journalArticle

Standard

SOLAR: An automated deduction system for consequence finding. / Nabeshima, Hidetomo; Iwanuma, Koji; Inoue, Katsumi; Ray, Oliver.

In: AI Communications, Vol. 23, No. 2-3, 183-203, 2010.

Research output: Contribution to journalArticle

Harvard

Nabeshima, H, Iwanuma, K, Inoue, K & Ray, O 2010, 'SOLAR: An automated deduction system for consequence finding', AI Communications, vol. 23, no. 2-3, 183-203. https://doi.org/10.3233/AIC-2010-0465

APA

Nabeshima, H., Iwanuma, K., Inoue, K., & Ray, O. (2010). SOLAR: An automated deduction system for consequence finding. AI Communications, 23(2-3), [183-203]. https://doi.org/10.3233/AIC-2010-0465

Vancouver

Nabeshima H, Iwanuma K, Inoue K, Ray O. SOLAR: An automated deduction system for consequence finding. AI Communications. 2010;23(2-3). 183-203. https://doi.org/10.3233/AIC-2010-0465

Author

Nabeshima, Hidetomo ; Iwanuma, Koji ; Inoue, Katsumi ; Ray, Oliver. / SOLAR: An automated deduction system for consequence finding. In: AI Communications. 2010 ; Vol. 23, No. 2-3.

Bibtex

@article{07129abd8ff249c0b7f61876b8888e36,
title = "SOLAR: An automated deduction system for consequence finding",
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.",
author = "Hidetomo Nabeshima and Koji Iwanuma and Katsumi Inoue and Oliver Ray",
note = "Other identifier: 2001174",
year = "2010",
doi = "10.3233/AIC-2010-0465",
language = "English",
volume = "23",
journal = "AI Communications",
issn = "0921-7126",
publisher = "IOS Press",
number = "2-3",

}

RIS - suitable for import to EndNote

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 -