Inductive theorem proving in theories specified by positive/negative-conditional equations
Claus-Peter Wirth, Ulrich Kühler · 1999
: 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. This research was supported by the Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt) C...