A comprehensive combination framework

DOI10.1145/1342991.1342992MaRDI QIDQ5277797zbMATH OpenOpenAlexFDO

Authors Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli

Publication date 12 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1342991.1342992

zbMATH Keywords

combinationdecision proceduresdescription logichigher-order logicmodal logicsatisfiability modulo theory

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27)

Recommendations

• Frontiers of Combining Systems
• Combinations of Theories for Decidable Fragments of First-Order Logic
• Unions of non-disjoint theories and combinations of satisfiability procedures
• Model-theoretic methods in combined constraint satisfiability
• Combination of disjoint theories: beyond decidability

Cited in

(14)

• Combination of convex theories: modularity, deduction completeness, and explanation
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• A unified and composable take on ratcheting
• Model completeness, covers and superposition
• Combining WS1S and HOL
• Combining theories: the Ackerman and guarded fragments
• Modular termination and combinability for superposition modulo counter arithmetic
• Satisfiability modulo theories
• Noetherianity and Combination Problems
• Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
• Data structures with arithmetic constraints: A non-disjoint combination
• Combinable Extensions of Abelian Groups
• Frontiers of Combining Systems
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs

This page was built for publication: A comprehensive combination framework

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