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