ISSN:
0949-2925
Keywords:
Schlüsselwörter: Klausale Spezifikation, partiell definierte Operatoren, hierarchische Termersetzungssysteme, induktives Beweisen
;
Key words: Clausal specification, partially defined operators, hierarchical term rewriting, inductive theorem proving.
;
CR Classification:F.3.1, F.3.2, F.4.1.
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Description / Table of Contents:
Abstract. Clausal specifications for the description of systems on the functional design level are studied. The axioms of such a specification $spec$ are positive/negative conditional equations which define new operators over a built-in algebra ${\cal A}$ . We define the semantics of $spec$ by an algebra ${\cal A}_{spec}$ which is initial in the class of all models which preserve ${\cal A}$ . An inference system for proving validity of clauses in ${\cal A}_{spec}$ is provided which also allows to refute non valid clauses.
Notes:
Zusammenfassung. In der Arbeit werden klausale Spezifikationen zur Beschreibung von Programmen auf der Ebene des funktionalen Entwurfs betrachtet. Die Axiome solch einer Spezifikation $spec$ bestehen aus positiv/negativ bedingten Gleichungen, die neue Operatoren über einer fest eingebauten Algebra ${\cal A}$ definieren. Wir definieren als Semantik von $spec$ eine Algebra ${\cal A}_{spec}$ , die initial in der Klasse aller Modelle ist. Es wird ein Inferenzsystem angegeben, mit dem man die Gültigkeit von positiv/negativ bedingten Gleichungen in ${\cal A}_{spec}$ beweisen kann. Dieses Inferenzsystem erlaubt es auch, die Gültigkeit von Behauptungen zu widerlegen.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/s004500050042
Permalink