scientific article; zbMATH DE number 1140674
From MaRDI portal
Publication:4385439
zbMath0893.03001MaRDI QIDQ4385439
Cesare Tinelli, Mehdi T. Harandi
Publication date: 20 July 1998
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
consistencycorrectnessfirst-order theoriestheory combinationcombination of satisfiability proceduresnondeterministic versionequality sharingNelson-Oppen combination procedure
Decidability of theories and sets of sentences (03B25) Grammars and rewriting systems (68Q42) Abstract deductive systems (03B22) Basic properties of first-order languages and structures (03C07)
Related Items
Strategies for combining decision procedures, Combining Theories: The Ackerman and Guarded Fragments, Sharing Is Caring: Combination of Theories, Satisfiability Modulo Theories, A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited, Modularity results for interpolation, amalgamation and superamalgamation, Combining nonstably infinite theories, Optimization Modulo Theories with Linear Rational Costs, Constraint solving for finite model finding in SMT solvers, Deciding the word problem in the union of equational theories., Modular instantiation schemes, Modular proof systems for partial functions with Evans equality, Efficient theory combination via Boolean search, Decision procedures for term algebras with integer constraints, Combining decision procedures by (model-)equality propagation, A decidability result for the model checking of infinite-state systems, Being careful about theory combination, Partition-based logical reasoning for first-order and propositional theories, Many-sorted equivalence of shiny and strongly polite theories, Quantifier-free interpolation in combinations of equality interpolating theories, An efficient SMT solver for string constraints, Quantifier Elimination and Provers Integration, Combining Non-Stably Infinite Theories, Canonization for disjoint unions of theories, Automatic decidability and combinability, Combining Decision Procedures by (Model-)Equality Propagation, Model-theoretic methods in combined constraint satisfiability, Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates, Politeness and combination methods for theories with bridging functions, A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method, Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis, Combinations of Theories for Decidable Fragments of First-Order Logic, Combination of uniform interpolants via Beth definability, Combined covers and Beth definability, Unions of non-disjoint theories and combinations of satisfiability procedures
