Combinations of Theories for Decidable Fragments of First-Order Logic
From MaRDI portal
Recommendations
- Decidable fragments of first-order modal logics
- Decidable and undecidable fragments of first-order concatenation theory
- Decidability of logical theories and their combination
- Lindstrom theorems for fragments of first-order logic
- Decidable fragments of many-sorted logic
- Decidable Fragments of Many-Sorted Logic
- Combination of disjoint theories: beyond decidability
- Fragments of First-Order Logic
- Completeness and decidability of general first-order logic (with a detour through the guarded fragment)
- On the relationship between the complexity of decidability and decomposability of first-order theories
Cites work
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Combining nonstably infinite theories
- Combining theories with shared set operations
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 3715502 (Why is no real title available?)
- scientific article; zbMATH DE number 3467028 (Why is no real title available?)
- scientific article; zbMATH DE number 1140674 (Why is no real title available?)
- scientific article; zbMATH DE number 1956575 (Why is no real title available?)
- scientific article; zbMATH DE number 1765681 (Why is no real title available?)
- scientific article; zbMATH DE number 1390334 (Why is no real title available?)
- scientific article; zbMATH DE number 965572 (Why is no real title available?)
- Normal form transformations
- On the Decision Problem for Two-Variable First-Order Logic
- Simplification by Cooperating Decision Procedures
- The B-Book
- The state of CASC
- Unions of non-disjoint theories and combinations of satisfiability procedures
Cited in
(24)- A full first-order constraint solver for decomposable theories
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Politeness and stable infiniteness: stronger together
- Polite combination of algebraic datatypes
- Politeness for the theory of algebraic datatypes
- On interpolation in automated theorem proving
- Combination of disjoint theories: beyond decidability
- A rewriting approach to the combination of data structures with bridging theories
- Combining theories: the Ackerman and guarded fragments
- Noetherianity and Combination Problems
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Combining theories with shared set operations
- On deciding satisfiability by theorem proving with speculative inferences
- scientific article; zbMATH DE number 2043527 (Why is no real title available?)
- A decidable fragment of second order logic with applications to synthesis
- A comprehensive combination framework
- Combining stable infiniteness and (strong) politeness
- Feferman-vaught decompositions for prefix classes of first order logic
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- On the convexity of a fragment of pure set theory with applications within a Nelson-Oppen framework
- Many-sorted equivalence of shiny and strongly polite theories
- Number theory combination: natural density and SMT
- Combining combination properties. I: Nelson-Oppen and politeness
- Being polite is not enough (and other limits of theory combination)
This page was built for publication: Combinations of Theories for Decidable Fragments of First-Order Logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3655205)
