Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving Ulrich Kuehler, Claus-Peter Wirth Fachbereich Informatik, Universitaet Kaiserslautern D-67663 Kaiserslautern Germany E-mail: {kuehler,wirth}@informatik.uni-kl.de Abstract We propose a specification language for the formalization of data types with partial or non-terminating operations as part of a rewrite-based logical framework for inductive theorem proving. The language requires constructors for designating data items and admits positive/negative conditional equations as axioms in specifications. The (total algebra) semantics for such specifications is based on so-called data models. We present admissibility conditions that guarantee the unique existence of a distinguished data model with properties similar to those of the initial model of a usual equational specification. Since admissibility of a specification requires confluence of the induced rewrite relation, we provide an effectively testable confluence criterion which does not presuppose termination. Keywords Algebraic specification, partial operations, conditional rewriting, confluence, inductive theorem proving Source anonymous FTP server ftp.uni-kl.de [131.246.94.94] path: /reports_uni-kl/computer_science/SEKI/1996/ file: Kuehler.SR-96-11.ps.gz