Ulrich Kühler, Claus-Peter Wirth
Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving
Bibtex Entry
Long Version:
SEKI-Report SR-1996-11
Full paper: Format: ps.gz.
Short version:
8th RTA 1997, LNCS 1232, pp. 38--52, Springer.
Full paper: Format: ps.gz.
Copyright Owner
Long Version:
Short version:
Yes! (Dec 31, 2007)
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.
Algebraic specification, partial operations, conditional rewriting, confluence, inductive theorem proving