A gentle non-disjoint combination of satisfiability procedures

DOI10.1007/978-3-319-08587-6_9zbMATH Open1423.68441OpenAlexW2210320991MaRDI QIDQ3192185FDOQ3192185

Christophe Ringeissen, Pascal Fontaine, Paula Chocron

Publication date: 26 September 2014

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-08587-6_9

Recommendations

• Unions of non-disjoint theories and combinations of satisfiability procedures
• Model-theoretic methods in combined constraint satisfiability
• A polite non-disjoint combination method: theories with bridging functions revisited
• Combining nonstably infinite theories
• Combining non-stably infinite theories

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic in artificial intelligence (68T27) Combined logics (03B62)

Cited In (7)

• Many-sorted equivalence of shiny and strongly polite theories
• Spectra and satisfiability for logics with successor and a unary function
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• Politeness and combination methods for theories with bridging functions
• Combining preorder and postorder resolution in a satisfiability solver
• A Rewriting Approach to the Combination of Data Structures with Bridging Theories
• A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited

This page was built for publication: A gentle non-disjoint combination of satisfiability procedures

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