Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving

  • We propose a specification language for the formalization of data types with par-tial or non-terminating operations as part of a rewrite-based logical frameworkfor inductive theorem proving. The language requires constructors for designat-ing data items and admits positive/negative conditional equations as axioms inspecifications. The (total algebra) semantics for such specifications is based onso-called data models. We present admissibility conditions that guarantee theunique existence of a distinguished data model with properties similar to thoseof the initial model of a usual equational specification. Since admissibility of aspecification requires confluence of the induced rewrite relation, we provide aneffectively testable confluence criterion which does not presuppose termination.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Ulrich Kühler, Claus-Peter Wirth
URN (permanent link):urn:nbn:de:hbz:386-kluedo-3672
Serie (Series number):SEKI Report (96,11)
Document Type:Preprint
Language of publication:English
Year of Completion:1999
Year of Publication:1999
Publishing Institute:Technische Universität Kaiserslautern
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $