- Authors
- Ulrich Kühler,
Claus-Peter Wirth
- Title
- Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving
Bibtex Entry
- In
-
- 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:
- SEKI
- Short version:
- Springer
- 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