Term rewriting induction
From MaRDI portal
Recommendations
Cites work
- Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
- Completion of a Set of Rules Modulo a Set of Equations
- Computing ground reducibility and inductively complete positions
- Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
- Data Types as Lattices
- scientific article; zbMATH DE number 3956434 (Why is no real title available?)
- scientific article; zbMATH DE number 4047063 (Why is no real title available?)
- scientific article; zbMATH DE number 4074541 (Why is no real title available?)
- scientific article; zbMATH DE number 4078851 (Why is no real title available?)
- scientific article; zbMATH DE number 3684925 (Why is no real title available?)
- scientific article; zbMATH DE number 3688776 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- scientific article; zbMATH DE number 3351184 (Why is no real title available?)
- On ground-confluence of term rewriting systems
- Orderings for term-rewriting systems
- Proving termination with multiset orderings
- Rewriting techniques for program synthesis
Cited in
(38)- How to prove equivalence of term rewriting systems without induction
- Deductive and inductive synthesis of equational programs
- Induction = I-axiomatization + first-order consistency.
- Induction using term orders
- Unprovability results for clause set cycles
- Induction and Skolemization in saturation theorem proving
- Transforming orthogonal inductive definition sets into confluent term rewrite systems
- On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs
- scientific article; zbMATH DE number 1722694 (Why is no real title available?)
- Induction for termination with local strategies
- Narrowing and rewriting logic: from foundations to applications
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- scientific article; zbMATH DE number 4164140 (Why is no real title available?)
- Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
- Dealing with Non-orientable Equations in Rewriting Induction
- scientific article; zbMATH DE number 4047062 (Why is no real title available?)
- scientific article; zbMATH DE number 125892 (Why is no real title available?)
- scientific article; zbMATH DE number 1231662 (Why is no real title available?)
- scientific article; zbMATH DE number 2043540 (Why is no real title available?)
- Termination of algorithms over non-freely generated data types
- Proofs in parameterized specifications
- Program transformation and rewriting
- Mechanically certifying formula-based Noetherian induction reasoning
- Improving rewriting induction approach for proving ground confluence
- Proof Terms for Infinitary Rewriting
- Induction using term orderings
- Mechanizable inductive proofs for a class of \(\forall \exists\) formulas
- Conditional rewriting in focus
- A general framework to build contextual cover set induction provers
- Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting
- Higher-order proof by consistency
- Transforming concurrent programs with semaphores into logically constrained term rewrite systems
- Using induction and rewriting to verify and complete parameterized specifications
- Difference of constrained patterns in logically constrained term rewrite systems
- A unified view of induction reasoning for first-order logic
- A verified algorithm for deciding pattern completeness
- A verified algorithm for deciding pattern completeness with optimal asymptotic complexity
- Arboretum for a generalisation of Ramanujan polynomials
This page was built for publication: Term rewriting induction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6488529)
