Modular Termination and Combinability for Superposition Modulo Counter Arithmetic

DOI10.1007/978-3-642-24364-6_15zbMath1348.68223OpenAlexW2125573666MaRDI QIDQ3172895

Christophe Ringeissen, Valerio Senni

Publication date: 7 October 2011

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-24364-6_15

Mathematics Subject Classification ID

Logic in computer science (03B70) Data structures (68P05)

Cites Work

• Unnamed Item
• Unnamed Item
• Automatic decidability and combinability
• Model-theoretic methods in combined constraint satisfiability
• Theory decision by decomposition
• A rewriting approach to satisfiability procedures.
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator
• Data Structures with Arithmetic Constraints: A Non-disjoint Combination
• Simplification by Cooperating Decision Procedures
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• Combinable Extensions of Abelian Groups
• Locality Results for Certain Extensions of Theories with Bridging Functions
• Decision procedures for algebraic data types with abstractions
• A comprehensive combination framework
• New results on rewrite-based satisfiability procedures
• Automatic Combinability of Rewriting-Based Satisfiability Procedures
• Verifying Balanced Trees
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures

This page was built for publication: Modular Termination and Combinability for Superposition Modulo Counter Arithmetic