Authors

Title

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

In

SEKI Report SR-95-15, Univ. Kaiserslautern, 1995

Up-to-dateness

This report is completely obsolete, please do not read or cite it but take the newer version instead.

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.

Full paper

Format: .ps.gz
Size: 301 Kbytes