Combinations of Theories for Decidable Fragments of First-Order Logic

DOI10.1007/978-3-642-04222-5_16zbMath1193.03020OpenAlexW1535925611MaRDI 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

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20) Combined logics (03B62)

Related Items (13)

Combining Theories: The Ackerman and Guarded Fragments ⋮ Combining stable infiniteness and (strong) politeness ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ A Rewriting Approach to the Combination of Data Structures with Bridging Theories ⋮ 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 ⋮ Politeness and stable infiniteness: stronger together ⋮ Combinations of Theories for Decidable Fragments of First-Order Logic ⋮ Combining Theories with Shared Set Operations ⋮ Polite combination of algebraic datatypes ⋮ Politeness for the theory of algebraic datatypes ⋮ On interpolation in automated theorem proving

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

This page was built for publication: Combinations of Theories for Decidable Fragments of First-Order Logic