Compilation of Recursive Two-Literal Clauses into Unification Algorithms

: Automated deduction systems can considerably be improved by replacing axioms with special purpose inference mechanisms. For example replacing in resolution based systems certain equations with theory unification algorithms reduces the amount of search because the algorithm introduces more determinism in the otherwise blind search strategy. Non-recursive clauses with two literals, i.e. clauses which do not resolve with a copy of themselves can be compiled automatically into a unification algorithm for literals which realizes a theory resolution with respect to the theory of the compiled clause. In this paper the compilation technique is extended to arbitrary clauses with two . The technique uses so called abstraction trees with continuations to represent potentially infinitely many self resolvents. These trees allow to detect easily how many copies of the compiled clause are necessary to (theory-) resolve two other clauses. Key words: Automated Deduction, Unification, Compilation of C...

• Type: Conference
• Year: 1990
• Where: AIMSA
• Authors: Hans Jürgen Ohlbach
• Keywords: AIMSA 1990, Artificial Intelligence, Automated Deduction, Theory Unification Algorithms, Unification Algorithm