Completion and Equational Theorem Proving using Taxonomic Constraints

Joerg Denzinger
Fachbereich Informatik, Universitaet Kaiserslautern
D-67663 Kaiserslautern, GERMANY
E-mail: denzinge@informatik.uni-kl.de

Abstract
We present an approach to prove several theorems in slightly different 
axiom systems simultaneously. We represent the different problems as 
a taxonomy, i.e. a tree in which each node inherits all knowledge of 
its predecessors, and solve the problems using inference steps on 
rules and equations with simple constraints, i.e. words identifying 
nodes in the taxonomy. We demonstrate that a substantial gain can be
achieved by using taxonomic constraints, not only by avoiding the 
repetition of inference steps in the different problems but also by 
achieving run times that are much shorter than the accumulated run 
times when proving each problem separately.

Keywords
theorem proving, constraint completion, taxonomy

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1995/
file: Denzinger.SR-95-11.ps.gz