Rewrite-based decision procedures

DOI10.1016/J.ENTCS.2006.11.042zbMATH Open1277.68238OpenAlexW2023447392MaRDI QIDQ2864358FDOQ2864358

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

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

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)

Cites Work

• Title not available (Why is that?)
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
• Title not available (Why is that?)
• Title not available (Why is that?)
• A rewriting approach to satisfiability procedures.
• Rewriting
• Rewrite-based satisfiability procedures for recursive data structures
• Computer Aided Verification
• Paramodulation-based theorem proving
• Frontiers of Combining Systems
• Computer Aided Verification
• Title not available (Why is that?)
• Theory and Applications of Satisfiability Testing

Cited In (13)

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

Uses Software

• CVC Lite
• CVC

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)