Quantifier Elimination and Provers Integration

DOI10.1016/S1571-0661(04)80650-9zbMath1261.68100MaRDI QIDQ4916219

Silvio Ghilardi

Publication date: 19 April 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

quantifier eliminationfusionmodel completionssuperposition calculusNelson-oppen combination schema

Mathematics Subject Classification ID

Quantifier elimination, model completeness, and related topics (03C10)

Related Items (4)

Combining nonstably infinite theories ⋮ Combining Non-Stably Infinite Theories ⋮ Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas ⋮ Combining sets with cardinals

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Complexity, convexity and combinations of theories
• Model theory.
• Model-companions and definability in existentially complete structures
• The computational complexity of logical theories
• Sheaves, games, and model completions. A categorical approach to nonclassical propositional logics
• A general setting for flexibly combining and augmenting decision procedures
• Cooperation of background reasoners in theory reasoning by residue sharing
• Unions of non-disjoint theories and combinations of satisfiability procedures
• Simplification by Cooperating Decision Procedures
• Reasoning About Recursively Defined Data Structures

This page was built for publication: Quantifier Elimination and Provers Integration