Simplification by Cooperating Decision Procedures
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A semantic approach to interpolation
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Theory decision by decomposition
- Combination of convex theories: modularity, deduction completeness, and explanation
- A decision procedure for combinations of propositional temporal logic and other specialized theories
- A structure-preserving clause form translation
- Unification in combinations of collapse-free regular theories
- Combination of constraint solvers for free and quasi-free structures
- Complexity, convexity and combinations of theories
- Natural language syntax and first-order inference
- An overview of the Tecton proof system
- 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.
- Virtual worlds as meeting places for formal systems
- Constraint contextual rewriting.
- Towards an integration science. The influence of Richard Bellman on our research.
- Solving linear optimization over arithmetic constraint formula
- Editors' introduction to the special issue on combining logics
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Structured proof procedures
- Sharpening constraint programming approaches for bit-vector theory
- IPL: an integration property language for multi-model cyber-physical systems
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- Tractable combinations of theories via sampling
- Politeness and stable infiniteness: stronger together
- Polite combination of algebraic datatypes
- Combination of uniform interpolants via Beth definability
- Combined covers and Beth definability
- Politeness for the theory of algebraic datatypes
- 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
- Automated generation of exam sheets for automated deduction
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Interpolation and amalgamation for arrays with MaxDiff
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Politeness and combination methods for theories with bridging functions
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Unification modulo lists with reverse relation with certain word equations
- On interpolation in automated theorem proving
- A decision procedure for (co)datatypes in SMT solvers
- Strategies for combining decision procedures
- Metalevel algorithms for variant satisfiability
- A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
- Modular proof systems for partial functions with Evans equality
- Efficient theory combination via Boolean search
- Decision procedures for term algebras with integer constraints
- A taxonomy of exact methods for partial Max-SAT
- Being careful about theory combination
- Partition-based logical reasoning for first-order and propositional theories
- Decision procedures for extensions of the theory of arrays
- Canonization for disjoint unions of theories
- A randomized satisfiability procedure for arithmetic and uninterpreted function symbols
- An interpolating theorem prover
- A tool for deciding the satisfiability of continuous-time metric temporal logic
- Modularity results for interpolation, amalgamation and superamalgamation
- Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages
- Order-Sorted Rewriting and Congruence Closure
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Colors Make Theories Hard
- Metalevel algorithms for variant satisfiability
- Model-based theory combination
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
- An abstract decision procedure for satisfiability in the theory of recursive data types
- Applications of hierarchical reasoning in the verification of complex systems
- Programmed strategies for program verification
- Proof tree preserving tree interpolation
- Distributing the workload in a lazy theorem-prover
- Interpolation systems for ground proofs in automated deduction: a survey
- A heuristic prover for real inequalities
- Decision procedures for region logic
- On First-Order Model-Based Reasoning
- Optimization modulo theories with linear rational costs
- Adapting real quantifier elimination methods for conflict set computation
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
- On interpolation in decision procedures
- Decision Procedures for Automating Termination Proofs
- Modular SMT proofs for fast reflexive checking inside Coq
- Combining theories: the Ackerman and guarded fragments
- A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
- Sharing is caring: combination of theories
- Modular termination and combinability for superposition modulo counter arithmetic
- Satisfiability modulo theories
- Combining Model Checking and Deduction
- On the cooperation of the constraint domains ℋ, ℛ, and ℱ in CFLP
- Interpolation for predefined types
- A decision procedure for (co)datatypes in SMT solvers
- A polite non-disjoint combination method: theories with bridging functions revisited
- Rewriting modulo SMT and open system analysis
- Verifying Heap-Manipulating Programs in an SMT Framework
- Ground Interpolation for the Theory of Equality
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- Efficient Term-ITE Conversion for Satisfiability Modulo Theories
- Combining equational reasoning
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Data structures with arithmetic constraints: A non-disjoint combination
- Combining theories with shared set operations
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)
