• Test message This is a test.
    投稿: 2008/08/26 5:43、Hidetomo NABESHIMA
1 - 1 / 1 件の投稿を表示中 もっと見る »


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.