Combining theories with shared set operations
From MaRDI portal
Recommendations
Cites work
- An introduction to mathematical logic and type theory: To truth through proof.
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Combined Satisfiability Modulo Parametric Theories
- Combining nonstably infinite theories
- Combining theories with shared set operations
- Combining WS1S and HOL
- Complexity of the two-variable fragment with counting quantifiers
- Computer Aided Verification
- Cooperating theorem provers: a case study combining HOL-Light and CVC Lite
- Deciding Boolean algebra with Presburger arithmetic
- Decision Procedures for Multisets with Cardinality Constraints
- Generalized finite automata theory with an application to a decision problem of second-order logic
- scientific article; zbMATH DE number 4112064 (Why is no real title available?)
- scientific article; zbMATH DE number 2038747 (Why is no real title available?)
- scientific article; zbMATH DE number 2080047 (Why is no real title available?)
- scientific article; zbMATH DE number 965572 (Why is no real title available?)
- Linear Arithmetic with Stars
- Model-theoretic methods in combined constraint satisfiability
- On Context-Free Languages
- Semigroups, Presburger formulas, and languages
- Simplification by Cooperating Decision Procedures
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- The first order properties of products of algebraic systems
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- Unions of non-disjoint theories and combinations of satisfiability procedures
Cited in
(20)- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Politeness and combination methods for theories with bridging functions
- On automation in the verification of software barriers: experience report
- Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
- Automated reasoning with restricted intensional sets
- Sets with cardinality constraints in satisfiability modulo theories
- Logical theories and compatible operations
- Combining theories: the Ackerman and guarded fragments
- A polite non-disjoint combination method: theories with bridging functions revisited
- Ordered sets in the calculus of data structures
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Combining theories with shared set operations
- Building a calculus of data structures
- On deciding satisfiability by theorem proving with speculative inferences
- scientific article; zbMATH DE number 2090060 (Why is no real title available?)
- scientific article; zbMATH DE number 2090084 (Why is no real title available?)
- Frontiers of Combining Systems
- On algebraic array theories
- Succinct ordering and aggregation constraints in algebraic array theories
- Polite combination in parametric array theories
This page was built for publication: Combining theories with shared set operations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3655212)
