And-Or Graphs Applied to RUE Resolution

In equality-based binary r e s o l u t i o n , the v i a b i l i t y t e s t is used as a decision mechanism to select disagreement sets and also to define the RUE u n i f i e r . In t h i s paper we solve the problem of non-termination of the v i a b i l i t y t e s t by applying the theory of And-Or graphs. RUE r e f u t a t i o n s are succinct and t y p i c a l l y less than h a l f as long as corresponding r e f u t a t i o n s w i t h the e q u a l i t y axioms. Furthermore, RUE r e s o l u t i o n is complete without using paramodulation or the e q u a l i t y axioms. Experiments w i t h a theorem prover based on t h i s method have produced superior r e s u l t s which are described in [ D i g r i c o l i and Harrison,1986].

• Type: Conference
• Year: 1989
• Where: IJCAI
• Authors: Vincent J. Digricoli, James J. Lu, V. S. Subrahmanian
• Keywords: Decision Mechanism, Disagreement Sets, IJCAI 1989, IJCAI 2007, Paper