Complete Pruning Methods and a Practical Search Strategy for SOL

WORKSHOP TO DEFINE DECONTAMINATION AND DECOMMISSIONING NEEDS FOR THE U.S. DEPARTMENT OF ENERGY

Hidetomo Nabeshima ; Koji Iwanuma ; Katsumi Inoue

Others  :  http://CEUR-WS.org/Vol-418/paper9.pdf
PID  :  3474

来源: CEUR

【 摘 要 】

The ability to find non-trivial consequences of an axiom set is useful in many applications of AI such as theorem proving, query answering and nonmonotonic reasoning. SOL (Skip Ordered Linear) calculus is one of the most significant calculi for consequence finding, which is complete for finding the non-subsumed consequences of a clausal theory. In this paper, we propose new complete pruning methods and a practical search strategy for SOL tableaux. These methods are indispensable for practical use in many application areas. The experimental results show that these techniques improve the performance of consequence finding process greatly.