Simplification by Cooperating Decision Procedures
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Ground Interpolation for the Theory of Equality
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Decision procedures for extensions of the theory of arrays
- Verifying Heap-Manipulating Programs in an SMT Framework
- Many-sorted equivalence of shiny and strongly polite theories
- On Hierarchical Reasoning in Combinations of Theories
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Reasoning about vectors using an SMT theory of sequences
- Generalised graded interpolation
- Symbolic computation in Maude: some tapas
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Better answers to real questions
- Canonization for disjoint unions of theories
- Succinct ordering and aggregation constraints in algebraic array theories
- Virtual worlds as meeting places for formal systems
- Being careful about theory combination
- DNN verification, reachability, and the exponential function problem
- Resolution proof transformation for compression and interpolation
- A taxonomy of exact methods for partial Max-SAT
- An abstract decision procedure for satisfiability in the theory of recursive data types
- Adapting real quantifier elimination methods for conflict set computation
- Producing and verifying extremely large propositional refutations
- On the completeness of interpolation algorithms
- Efficient theory combination via Boolean search
- On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP
- Efficient Term-ITE Conversion for Satisfiability Modulo Theories
- Modular termination and combinability for superposition modulo counter arithmetic
- Metalevel algorithms for variant satisfiability
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- Constraint contextual rewriting.
- Optimization modulo theories with linear rational costs
- A structural/temporal query language for business processes
- Decision Procedures for Automating Termination Proofs
- Towards a dereversibilizer: fewer asserts, statically
- Combination of constraint solving techniques: An algebraic point of view
- A decision procedure for a sublanguage of set theory involving monotone, additive, and multiplicative functions. I: The two-level case
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- A structure-preserving clause form translation
- Common knowledge does not have the Beth property
- Interpolation and amalgamation for arrays with MaxDiff
- Complexity, convexity and combinations of theories
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
- Programmed strategies for program verification
- Proof tree preserving tree interpolation
- Interpolation systems for ground proofs in automated deduction: a survey
- A heuristic prover for real inequalities
- Model-theoretic methods in combined constraint satisfiability
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
- Combining Decision Procedures by (Model-)Equality Propagation
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- Automated generation of exam sheets for automated deduction
- Tractable combinations of temporal CSPs
- Combining decision procedures by (model-)equality propagation
- Combining theories: the Ackerman and guarded fragments
- A decidability result for the model checking of infinite-state systems
- Monotonicity inference for higher-order formulas
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- On deciding satisfiability by theorem proving with speculative inferences
- An extension of lazy abstraction with interpolation for programs with arrays
- Quantifier-free interpolation in combinations of equality interpolating theories
- Automatic decidability and combinability
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- An institution-independent proof of the Robinson consistency theorem
- IPL: an integration property language for multi-model cyber-physical systems
- Strategies for combining decision procedures
- On quasitautologies
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- A polite non-disjoint combination method: theories with bridging functions revisited
- Unification in a combination of arbitrary disjoint equational theories
- Combining nonstably infinite theories
- Combining combination properties: minimal models
- Combinable Extensions of Abelian Groups
- Reasoning about vectors: satisfiability modulo a theory of sequences
- On Shostak's decision procedure for combinations of theories
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Politeness and combination methods for theories with bridging functions
- A semantic approach to interpolation
- Theory decision by decomposition
- Partition-based logical reasoning for first-order and propositional theories
- Unification in combinations of collapse-free regular theories
- An empirical assessment of progress in automated theorem proving
- A decision procedure for combinations of propositional temporal logic and other specialized theories
- Combination of constraint solvers for free and quasi-free structures
- scientific article; zbMATH DE number 7199580 (Why is no real title available?)
- Combined covers and Beth definability
- Combining non-stably infinite theories
- Embedding complex decision procedures inside an interactive theorem prover.
- Deciding the word problem in the union of equational theories.
- A rewriting approach to satisfiability procedures.
- A randomized satisfiability procedure for arithmetic and uninterpreted function symbols
- Applications of hierarchical reasoning in the verification of complex systems
- Modular SMT proofs for fast reflexive checking inside Coq
- Modular constraint solver cooperation via abstract interpretation
- Combining stable infiniteness and (strong) politeness
- On First-Order Model-Based Reasoning
- Improving complex SMT strategies with learning
- An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty
- Structured proof procedures
- On combinations of local theory extensions
- Modularity results for interpolation, amalgamation and superamalgamation
This page was built for publication: Simplification by Cooperating Decision Procedures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3899468)
