Tools for proving inductive equalities, relative completeness, and -completeness
DOI10.1016/0890-5401(90)90033-EzbMATH Open0691.68026MaRDI QIDQ582891FDOQ582891
Authors: Azeddine Lazrek, Pierre Lescanne, Jean-Jacques Thiel 
Publication date: 1990
Published in: Information and Computation (Search for Journal in Brave)
Recommendations
functional programmingcompletenessunificationabstract data typesequational theoriesrewriting systemsinitial algebracall by matchingcompletion procedure
General topics in the theory of software (68N01) Symbolic computation and algebraic computation (68W30) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Thue and Post systems, etc. (03D03) Abstract data types; algebraic specification (68Q65)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- On sufficient-completeness and related properties of term rewriting systems
- The algebraic specification of abstract data types
- Title not available (Why is that?)
- Title not available (Why is that?)
- Proofs by induction in equational theories with constructors
- Proof by consistency
- Counterexamples to termination for the direct sum of term rewriting systems
- Equational problems and disunification
- Partial evaluation and \(\omega\)-completeness of algebraic specifications
- Semantic confluence tests and completion methods
- Title not available (Why is that?)
- Explicit representation of terms defined by counter examples
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The λ-calculus is ω-incomplete
- The Logic of Equality
- Abstract data types and software validation
Cited In (12)
- A proof method for local sufficient completeness of term rewriting systems
- Improving rewriting induction approach for proving ground confluence
- Proving weak properties of rewriting
- Basic notions of universal algebra for language theory and graph grammars
- Using induction and rewriting to verify and complete parameterized specifications
- An algebraic characterization of inductive soundness in proof by consistency
- Transforming orthogonal inductive definition sets into confluent term rewrite systems
- Which data types have \(\omega\)-complete initial algebra specifications?
- Sufficient completeness verification for conditional and constrained TRS
- On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs
- On finite alphabets and infinite bases
- Algebra and theory of order-deterministic pomsets
Uses Software
This page was built for publication: Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q582891)
