Rewriting Induction + Linear Arithmetic = Decision Procedure

DOI10.1007/978-3-642-31365-3_20zbMATH Open1358.68252OpenAlexW2171347031MaRDI QIDQ2908496FDOQ2908496

Deepak Kapur, Stephan Falke

Publication date: 5 September 2012

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://publikationen.bibliothek.kit.edu/1000025940

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Cited In (6)

• Generalized rewrite theories, coherence completion, and symbolic methods
• Rewriting modulo SMT and open system analysis
• Variant-Based Satisfiability in Initial Algebras
• Transforming concurrent programs with semaphores into logically constrained term rewrite systems
• Verifying Procedural Programs via Constrained Rewriting Induction
• Combining induction and saturation-based theorem proving

Uses Software

• cvc3

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• An even closer integration of linear arithmetic into inductive theorem proving 👍 👎
• Rewrite-based decision procedures 👍 👎
• Term rewriting induction 👍 👎
• Induction in linear logic 👍 👎
• New uses of linear arithmetic in automated theorem proving by induction 👍 👎
• Proving and rewriting 👍 👎
• Rewriting with Linear Inferences in Propositional Logic 👍 👎
• Inductive Decidability Using Implicit Induction 👍 👎

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)