Combinations of Theories for Decidable Fragments of First-Order Logic

DOI10.1007/978-3-642-04222-5_16zbMath1193.03020MaRDI QIDQ3655205

Pascal Fontaine

Publication date: 7 January 2010

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04222-5_16

Mathematics Subject Classification ID

03B25: Decidability of theories and sets of sentences

03B35: Mechanization of proofs and logical operations

03B20: Subsystems of classical logic (including intuitionistic logic)

03B62: Combined logics

Related Items

On deciding satisfiability by theorem proving with speculative inferences, Many-sorted equivalence of shiny and strongly polite theories, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, On interpolation in automated theorem proving, A Rewriting Approach to the Combination of Data Structures with Bridging Theories, Combining Theories: The Ackerman and Guarded Fragments, Combinations of Theories for Decidable Fragments of First-Order Logic, Combining Theories with Shared Set Operations

Uses Software

• VAMPIRE
• E Theorem Prover

Cites Work

• Combining nonstably infinite theories
• Unions of non-disjoint theories and combinations of satisfiability procedures
• Combinations of Theories for Decidable Fragments of First-Order Logic
• Combining Theories with Shared Set Operations
• Simplification by Cooperating Decision Procedures
• The B-Book
• On the Decision Problem for Two-Variable First-Order Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item