Modular termination and combinability for superposition modulo counter arithmetic

DOI10.1007/978-3-642-24364-6_15MaRDI QIDQ3172895zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Theoretical Aspects of Computing – ICTAC 2005
• Combining satisfiability procedures for unions of theories with a shared counting operator
• Automated Reasoning
• Modular proof systems for partial functions with Evans equality
• Automatic Combinability of Rewriting-Based Satisfiability Procedures

Cites work

• A comprehensive combination framework
• A rewriting approach to satisfiability procedures.
• Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
• Automatic Combinability of Rewriting-Based Satisfiability Procedures
• Automatic decidability and combinability
• Combinable Extensions of Abelian Groups
• Combining satisfiability procedures for unions of theories with a shared counting operator
• Data structures with arithmetic constraints: A non-disjoint combination
• Decision procedures for algebraic data types with abstractions
• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• Locality Results for Certain Extensions of Theories with Bridging Functions
• Model-theoretic methods in combined constraint satisfiability
• New results on rewrite-based satisfiability procedures
• On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
• On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Rewriting
• Simplification by Cooperating Decision Procedures
• Theory decision by decomposition
• Verifying Balanced Trees

Cited in

(4)

• Termination modulo equations by abstract commutation with an application to iteration
• Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
• Automated Reasoning
• Theoretical Aspects of Computing – ICTAC 2005

This page was built for publication: Modular termination and combinability for superposition modulo counter arithmetic

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