Quantifier Elimination and Provers Integration
From MaRDI portal
Publication:4916219
DOI10.1016/S1571-0661(04)80650-9zbMath1261.68100MaRDI QIDQ4916219
Publication date: 19 April 2013
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
quantifier elimination; fusion; model completions; superposition calculus; Nelson-oppen combination schema
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