scientific article

zbMath0438.68043MaRDI QIDQ3880309

Joseph A. Goguen

Publication date: 1980

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

Knuth-Bendix algorithminitial algebrastructural inductionrewrite rulescorrectness of data type implementationdeciding the equivalence of expressionsinductive equational hypotheses

Mathematics Subject Classification ID

Related Items (38)

On sufficient-completeness and related properties of term rewriting systems ⋮ Conditional rewriting logic: Deduction, models and concurrency ⋮ Proof by consistency in conditional equational theories ⋮ Completion procedures as semidecision procedures ⋮ Gordon's computer: A hardware verification case study in OBJ3 ⋮ OBTAINING CONTRADICTION MEASURES ON INTUITIONISTIC FUZZY SETS FROM FUZZY CONNECTIVES ⋮ Proof by consistency ⋮ Inductive proofs by specification transformations ⋮ Rewriting with a nondeterministic choice operator ⋮ Equivalences and transformations of regular systems - applications to recursive program schemes and grammars ⋮ Simplifying conditional term rewriting systems: Unification, termination and confluence ⋮ History and basic features of the critical-pair/completion procedure ⋮ Automatic inductive theorem proving using Prolog ⋮ Sufficient-completeness, ground-reducibility and their complexity ⋮ Modular algebraic specification of some basic geometrical constructions ⋮ Induction using term orders ⋮ Proving and rewriting ⋮ Algebraic specification of concurrent systems ⋮ Algebraic implementation of abstract data types ⋮ Transformations and confluence for rewrite systems ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Conditional rewriting logic as a unified model of concurrency ⋮ Paramorphisms ⋮ Order-sorted unification ⋮ Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness ⋮ Induction using term orderings ⋮ On the connection between narrowing and proof by consistency ⋮ Schematization of infinite sets of rewrite rules generated by divergent completion processes ⋮ Automating inductionless induction using test sets ⋮ A strong restriction of the inductive completion procedure ⋮ Automatic proofs by induction in theories without constructors ⋮ Inductive proof search modulo ⋮ Proofs by induction in equational theories with constructors ⋮ Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories ⋮ Some fundamental algebraic tools for the semantics of computation: II. Signed and abstract theories ⋮ A superposition oriented theorem prover ⋮ Comparing data type specifications via their normal forms ⋮ The equational part of proofs by structural induction

This page was built for publication: