Rewrite-based decision procedures

DOI10.1016/J.ENTCS.2006.11.042MaRDI QIDQ2864358zbMATH OpenOpenAlexFDO

Authors Maria Paola Bonacina, Mnacho Echenim

Publication date 6 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.11.042

zbMATH Keywords

\(T\)-decision proceduresrewrite-based inference systems

Mathematics Subject Classification ID

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

Recommendations

• Rewrite-based satisfiability procedures for recursive data structures
• New results on rewrite-based satisfiability procedures
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
• A rewriting approach to satisfiability procedures.
• scientific article; zbMATH DE number 2086593

Cites work

• scientific article; zbMATH DE number 1614688 (Why is no real title available?)
• scientific article; zbMATH DE number 1903356 (Why is no real title available?)
• scientific article; zbMATH DE number 1903374 (Why is no real title available?)
• scientific article; zbMATH DE number 2090318 (Why is no real title available?)
• A rewriting approach to satisfiability procedures.
• Computer Aided Verification
• Computer Aided Verification
• Frontiers of Combining Systems
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
• Paramodulation-based theorem proving
• Rewrite-based satisfiability procedures for recursive data structures
• Rewriting
• Theory and Applications of Satisfiability Testing

Cited in

(13)

• Constructing Rewrite-Based Decision Procedures for Embeddings and Termination
• Locality Results for Certain Extensions of Theories with Bridging Functions
• Rewriting Induction + Linear Arithmetic = Decision Procedure
• On deciding satisfiability by theorem proving with speculative inferences
• New results on rewrite-based satisfiability procedures
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
• Theory decision by decomposition
• scientific article; zbMATH DE number 2086593 (Why is no real title available?)
• scientific article; zbMATH DE number 1639660 (Why is no real title available?)
• Mechanizing Mathematical Reasoning
• Rewrite-based satisfiability procedures for recursive data structures
• Frontiers of Combining Systems
• ${\mathcal{T}}$ -Decision by Decomposition

Describes a project that uses

Uses Software

• CVC
• CVC Lite

This page was built for publication: Rewrite-based decision procedures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864358)