Polite theories revisited

DOI10.1007/978-3-642-16242-8_29MaRDI QIDQ4933320zbMATH OpenOpenAlexFDO

Authors Dejan Jovanović, Clark Barrett

Publication date 12 October 2010

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-16242-8_29

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70)

Recommendations

• Politeness and combination methods for theories with bridging functions
• Revisiting the equivalence of shininess and politeness
• A polite non-disjoint combination method: theories with bridging functions revisited
• Combining nonstably infinite theories
• A gentle non-disjoint combination of satisfiability procedures

Cited in

(18)

• Many-sorted equivalence of shiny and strongly polite theories
• Reasoning about vectors using an SMT theory of sequences
• Being careful about theory combination
• Excuse me! or the courteous theatregoers' problem
• Revisiting the equivalence of shininess and politeness
• A rewriting approach to the combination of data structures with bridging theories
• A polite non-disjoint combination method: theories with bridging functions revisited
• Reasoning about vectors: satisfiability modulo a theory of sequences
• Politeness and combination methods for theories with bridging functions
• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
• Combining stable infiniteness and (strong) politeness
• Reasoning with finite sets and cardinality constraints in SMT
• Satisfiability modulo theories
• Politeness and stable infiniteness: stronger together
• Politeness for the theory of algebraic datatypes
• Sharing is caring: combination of theories
• Combining Finite Combination Properties: Finite Models and Busy Beavers
• Polite combination of algebraic datatypes

This page was built for publication: Polite theories revisited

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