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