Inductive Theorem Proving in Theories Specified by 
Positive/Negative-Conditional Equations

Claus-Peter Wirth and Ulrich Kuehler
Fachbereich Informatik
Universitaet Kaiserslautern
D-67663 Kaiserslautern 
Germany

Abstract
We present an inference system for clausal theorem 
proving w.r.t. various kinds of inductive validity 
in theories specified by constructor-based 
positive/negative-conditional equations.
The reduction relation defined by such equations has to 
be (ground) confluent, but need not be terminating.
Our constructor-based approach is well-suited for 
inductive theorem proving in the presence of partially 
defined functions.
The proposed inference system provides explicit 
induction hypotheses and can be instantiated with 
various wellfounded induction orderings.
While emphasizing a well structured clear design 
of the inference system,
our fundamental design goal is user-orientation and 
practical usefulness rather than theoretical elegance.
The resulting inference system is comprehensive and 
relatively powerful, but requires a sophisticated 
concept of proof guidance, which is not treated in this 
paper.

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