Rewriting Induction + Linear Arithmetic = Decision Procedure
From MaRDI portal
Recommendations
- scientific article; zbMATH DE number 1639660
- Induction in linear logic
- Term rewriting induction
- Inductive Decidability Using Implicit Induction
- An even closer integration of linear arithmetic into inductive theorem proving
- Rewrite-based decision procedures
- Rewriting with linear inferences in propositional logic
- New uses of linear arithmetic in automated theorem proving by induction
- scientific article; zbMATH DE number 785049
- Proving and rewriting
Cited in
(11)- Generalized rewrite theories, coherence completion, and symbolic methods
- Verifying procedural programs via constrained rewriting induction
- Some techniques for reasoning automatically on co-inductive data structures
- scientific article; zbMATH DE number 1614706 (Why is no real title available?)
- scientific article; zbMATH DE number 1765694 (Why is no real title available?)
- Rewriting modulo SMT and open system analysis
- A verified algorithm for deciding pattern completeness
- scientific article; zbMATH DE number 1639660 (Why is no real title available?)
- Variant-Based Satisfiability in Initial Algebras
- Transforming concurrent programs with semaphores into logically constrained term rewrite systems
- Combining induction and saturation-based theorem proving
This page was built for publication: Rewriting Induction + Linear Arithmetic = Decision Procedure
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2908496)
