Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness

DOI10.1016/0890-5401(90)90033-EzbMath0691.68026MaRDI QIDQ582891

Pierre Lescanne, Azeddine Lazrek, Jean-Jacques Thiel

Publication date: 1990

Published in: Information and Computation (Search for Journal in Brave)

zbMATH Keywords

completenessunificationrewriting systemsfunctional programmingabstract data typesequational theoriesinitial algebracall by matchingcompletion procedure

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Data structures (68P05) General topics in the theory of software (68N01) Thue and Post systems, etc. (03D03)

Related Items

A proof method for local sufficient completeness of term rewriting systems ⋮ Transforming orthogonal inductive definition sets into confluent term rewrite systems ⋮ On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs ⋮ Sufficient completeness verification for conditional and constrained TRS ⋮ On finite alphabets and infinite bases ⋮ Basic notions of universal algebra for language theory and graph grammars ⋮ Using induction and rewriting to verify and complete parameterized specifications ⋮ Proving weak properties of rewriting ⋮ Algebra and theory of order-deterministic pomsets ⋮ Improving rewriting induction approach for proving ground confluence ⋮ Which data types have \(\omega\)-complete initial algebra specifications?

Uses Software

• Miranda

Cites Work

• Proofs by induction in equational theories with constructors
• On sufficient-completeness and related properties of term rewriting systems
• Partial evaluation and \(\omega\)-completeness of algebraic specifications
• Proof by consistency
• Explicit representation of terms defined by counter examples
• Counterexamples to termination for the direct sum of term rewriting systems
• Equational problems and disunification
• The algebraic specification of abstract data types
• Semantic confluence tests and completion methods
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• The λ-calculus is ω-incomplete
• The Logic of Equality
• Abstract data types and software validation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item