Inductive theorem proving in theories specified by positive/negative-conditional equations

• We present an inference system for clausal theorem proving w.r.t. various kinds of inductivevalidity in theories specified by constructor-based positive/negative-conditional equations. The reductionrelation defined by such equations has to be (ground) confluent, but need not be terminating. Our con-structor-based approach is well-suited for inductive theorem proving in the presence of partially definedfunctions. The proposed inference system provides explicit induction hypotheses and can be instantiatedwith various wellfounded induction orderings. While emphasizing a well structured clear design of theinference system, our fundamental design goal is user-orientation and practical usefulness rather thantheoretical elegance. The resulting inference system is comprehensive and relatively powerful, but requiresa sophisticated concept of proof guidance, which is not treated in this paper.This research was supported by the Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt)

Additional Services

Author: Claus-Peter Wirth, Ulrich Kühler urn:nbn:de:hbz:386-kluedo-3561 SEKI Report (95,15) Preprint English 1999 1999 Technische Universität Kaiserslautern 2000/04/03 Fachbereich Informatik 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581$