- Claus-Peter Wirth,
- Inductive Theorem Proving in Theories Specified by Positive/Negative-Conditional Equations
- SEKI Report SR-95-15, Univ. Kaiserslautern, 1995
- This report is completely obsolete, please do not read or cite it but
take the newer version instead.
We present an inference system for clausal theorem
proving w.r.t. various kinds of inductive validity
in theories specified by constructor-based
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
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
- Full paper
- 301 Kbytes