Combining nonstably infinite theories
From MaRDI portal
Publication:851136
DOI10.1007/s10817-005-5204-9zbMath1108.03014OpenAlexW2056350513MaRDI QIDQ851136
Calogero G. Zarba, Cesare Tinelli
Publication date: 17 November 2006
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-005-5204-9
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Related Items
A decision procedure for (co)datatypes in SMT solvers ⋮ Decision procedures for flat array properties ⋮ Combining Theories: The Ackerman and Guarded Fragments ⋮ Satisfiability Modulo Theories ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Combining stable infiniteness and (strong) politeness ⋮ Modular instantiation schemes ⋮ A Rewriting Approach to the Combination of Data Structures with Bridging Theories ⋮ On the verification of security-aware E-services ⋮ Combining decision procedures by (model-)equality propagation ⋮ Symbolic backward reachability with effectively propositional logic. Application to security policy analysis ⋮ Parametrized invariance for infinite state processes ⋮ Many-sorted equivalence of shiny and strongly polite theories ⋮ Automatic decidability and combinability ⋮ On Hierarchical Reasoning in Combinations of Theories ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Politeness and stable infiniteness: stronger together ⋮ Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis ⋮ 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
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Complexity, convexity and combinations of theories
- Cooperation of background reasoners in theory reasoning by residue sharing
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Simplify: a theorem prover for program checking
- Simplification by Cooperating Decision Procedures
- Quantifier Elimination and Provers Integration
- Combining Non-Stably Infinite Theories
- A Decision Procedure for Monotone Functions over Bounded and Complete Lattices
- Automated Reasoning
- Formal Methods at the Crossroads. From Panacea to Foundational Support
This page was built for publication: Combining nonstably infinite theories
