zbMATH — the first resource for mathematics

SOLAR: a consequence finding system for advanced reasoning. (English) Zbl 1274.68412
Cialdea Mayer, Marta (ed.) et al., Automated reasoning with analytic tableaux and related methods. International conference TABLEAUX 2003, Rome, Italy, September 9–12, 2003. Proceedings. Berlin: Springer (ISBN 3-540-40787-1/pbk). Lect. Notes Comput. Sci. 2796, 257-263 (2003).
Summary: SOLAR is an efficient first-order consequence finding system based on a connection tableau format with Skip operation. Consequence finding 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. 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.
For the entire collection see [Zbl 1024.00047].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T27 Logic in artificial intelligence
Full Text: DOI