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 elimination; fusion; model completions; superposition calculus; Nelson-oppen combination schema

Mathematics Subject Classification ID

03C10: Quantifier elimination, model completeness, and related topics

Related Items

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

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