A gentle non-disjoint combination of satisfiability procedures

DOI10.1007/978-3-319-08587-6_9MaRDI QIDQ3192185zbMATH OpenOpenAlexFDO

Authors Paula Chocron, Pascal Fontaine, Christophe Ringeissen

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

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)

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

Cited in

(8)

• 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
• Polite theories revisited
• A rewriting approach to the combination of data structures with bridging theories
• A polite non-disjoint combination method: theories with bridging functions revisited
• Politeness and combination methods for theories with bridging functions
• Combining preorder and postorder resolution in a satisfiability solver

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)