Rewriting Induction + Linear Arithmetic = Decision Procedure

DOI10.1007/978-3-642-31365-3_20zbMath1358.68252OpenAlexW2171347031MaRDI QIDQ2908496

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

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

Related Items (5)

Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Rewriting modulo SMT and open system analysis ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Combining induction and saturation-based theorem proving

Uses Software

• cvc3

This page was built for publication: Rewriting Induction + Linear Arithmetic = Decision Procedure