Combining Theories with Shared Set Operations
From MaRDI portal
Publication:3655212
DOI10.1007/978-3-642-04222-5_23zbMath1193.03030OpenAlexW1747570770MaRDI QIDQ3655212
Viktor Kuncak, Thomas Wies, Ruzica Piskac
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_23
Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Combined logics (03B62)
Related Items
Combining Theories: The Ackerman and Guarded Fragments ⋮ A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ Automated reasoning with restricted intensional sets ⋮ On algebraic array theories ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Sets with Cardinality Constraints in Satisfiability Modulo Theories ⋮ Politeness and combination methods for theories with bridging functions ⋮ Combinations of Theories for Decidable Fragments of First-Order Logic ⋮ Combining Theories with Shared Set Operations ⋮ On automation in the verification of software barriers: experience report
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Model-theoretic methods in combined constraint satisfiability
- Combining nonstably infinite theories
- Deciding Boolean algebra with Presburger arithmetic
- An introduction to mathematical logic and type theory: To truth through proof.
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Semigroups, Presburger formulas, and languages
- Complexity of the two-variable fragment with counting quantifiers
- The first order properties of products of algebraic systems
- Linear Arithmetic with Stars
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Combining Theories with Shared Set Operations
- Simplification by Cooperating Decision Procedures
- Computer Aided Verification
- Decision Procedures for Multisets with Cardinality Constraints
- On Context-Free Languages
- Generalized finite automata theory with an application to a decision problem of second-order logic
- Combined Satisfiability Modulo Parametric Theories
