Tools for proving inductive equalities, relative completeness, and -completeness
From MaRDI portal
Publication:582891
Recommendations
Cites work
- scientific article; zbMATH DE number 3888893 (Why is no real title available?)
- scientific article; zbMATH DE number 3891336 (Why is no real title available?)
- scientific article; zbMATH DE number 4164142 (Why is no real title available?)
- scientific article; zbMATH DE number 3896335 (Why is no real title available?)
- scientific article; zbMATH DE number 3911679 (Why is no real title available?)
- scientific article; zbMATH DE number 3913659 (Why is no real title available?)
- scientific article; zbMATH DE number 3945335 (Why is no real title available?)
- scientific article; zbMATH DE number 3951980 (Why is no real title available?)
- scientific article; zbMATH DE number 3976991 (Why is no real title available?)
- scientific article; zbMATH DE number 4037164 (Why is no real title available?)
- scientific article; zbMATH DE number 4049024 (Why is no real title available?)
- scientific article; zbMATH DE number 4090765 (Why is no real title available?)
- scientific article; zbMATH DE number 3654207 (Why is no real title available?)
- scientific article; zbMATH DE number 3684925 (Why is no real title available?)
- scientific article; zbMATH DE number 3776841 (Why is no real title available?)
- scientific article; zbMATH DE number 3639689 (Why is no real title available?)
- Abstract data types and software validation
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Counterexamples to termination for the direct sum of term rewriting systems
- Equational problems and disunification
- Explicit representation of terms defined by counter examples
- On sufficient-completeness and related properties of term rewriting systems
- Partial evaluation and \(\omega\)-completeness of algebraic specifications
- Proof by consistency
- Proofs by induction in equational theories with constructors
- Semantic confluence tests and completion methods
- The Logic of Equality
- The algebraic specification of abstract data types
- The λ-calculus is ω-incomplete
Cited in
(12)- Transforming orthogonal inductive definition sets into confluent term rewrite systems
- Using induction and rewriting to verify and complete parameterized specifications
- Improving rewriting induction approach for proving ground confluence
- Proving weak properties of rewriting
- A proof method for local sufficient completeness of term rewriting systems
- Which data types have \(\omega\)-complete initial algebra specifications?
- On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs
- Algebra and theory of order-deterministic pomsets
- An algebraic characterization of inductive soundness in proof by consistency
- Basic notions of universal algebra for language theory and graph grammars
- Sufficient completeness verification for conditional and constrained TRS
- On finite alphabets and infinite bases
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)
