scientific article
From MaRDI portal
Publication:3880309
zbMath0438.68043MaRDI QIDQ3880309
Publication date: 1980
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Knuth-Bendix algorithminitial algebrastructural inductionrewrite rulescorrectness of data type implementationdeciding the equivalence of expressionsinductive equational hypotheses
Abstract data types; algebraic specification (68Q65) Mechanization of proofs and logical operations (03B35) Data structures (68P05) Algebraic structures (08A99)
Related Items
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
