Portal de Periódicos da CAPES

SOLAR: A Consequence Finding System for Advanced Reasoning

2003; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-540-45206-5_22

1611-3349

Hidetomo Nabeshima, Koji Iwanuma, Katsumi Inoue,

Semantic Web and Ontologies

SOLAR is an efficient first-order consequence finding system based on a connection tableau format with Skip operation. Consequence finding 1,2,3,4 is a generalization of refutation finding or theorem proving, and is useful for many reasoning tasks such as knowledge compilation, inductive logic programming, abduction. One of the most significant calculus of consequence finding is SOL 2. SOL is complete for consequence finding and can find all minimal-length consequences with respect to subsumption. SOLAR (SOL for Advanced Reasoning) is an efficient implementation of SOL and can avoid producing non-minimal/redundant consequences due to various state of the art pruning methods, such as skip-regularity, local failure caching, folding-up (see 5,6).