SOLAR: An automated deduction system for consequence finding
Hidetomo Nabeshima, Koji Iwanuma, Katsumi Inoue, Oliver Ray · AI Communications · 2010
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