Simplification by Cooperating Decision Procedures
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A tool for deciding the satisfiability of continuous-time metric temporal logic
- Colors Make Theories Hard
- scientific article; zbMATH DE number 7566058 (Why is no real title available?)
- Data structures with arithmetic constraints: A non-disjoint combination
- Combining theories with shared set operations
- Number theory combination: natural density and SMT
- Polite combination in parametric array theories
- Shininess, strong politeness, and unicorns
- Decision procedures for term algebras with integer constraints
- On interpolation in decision procedures
- A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Interpolation Results for Arrays with Length and MaxDiff
- Satisfiability checking: theory and applications
- Deciding Boolean algebra with Presburger arithmetic
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Solving constraint satisfaction problems with SAT modulo theories
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Satisfiability modulo theories
- Politeness and stable infiniteness: stronger together
- Tractable combinations of theories via sampling
- Combining combination properties. I: Nelson-Oppen and politeness
- Solving linear optimization over arithmetic constraint formula
- Politeness for the theory of algebraic datatypes
- Decision procedures for region logic
- Simplified and verified: a second look at a proof-producing union-find algorithm
- Being polite is not enough (and other limits of theory combination)
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Combination of convex theories: modularity, deduction completeness, and explanation
- Rewriting modulo SMT and open system analysis
- A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method
- Sharing is caring: combination of theories
- On the convexity of a fragment of pure set theory with applications within a Nelson-Oppen framework
- Editors' introduction to the special issue on combining logics
- A new combination procedure for the word problem that generalizes fusion decidability results in modal logics
- Combining Model Checking and Deduction
- On interpolation in automated theorem proving
- A decision procedure for (co)datatypes in SMT solvers
- Natural language syntax and first-order inference
- A decision procedure for (co)datatypes in SMT solvers
- Modular proof systems for partial functions with Evans equality
- Quantifier Elimination and Provers Integration
- Combining Finite Combination Properties: Finite Models and Busy Beavers
- Deciding theoremhood in fibered logics without shared connectives
- The CDSAT method for satisfiability modulo theories and assignment: an exposition
- An interpolating theorem prover
- The theorem prover of the program verifier Tatzelwurm
- Modular term rewriting systems and the termination
- An overview of the Tecton proof system
- Unification modulo lists with reverse relation with certain word equations
- Model-based theory combination
- Variant-Based Satisfiability in Initial Algebras
- Order-Sorted Rewriting and Congruence Closure
- Metalevel algorithms for variant satisfiability
- Sharpening constraint programming approaches for bit-vector theory
- Modular higher-order E-unification
- Interpolation for predefined types
- Variants and satisfiability in the infinitary unification wonderland
- Essence of generalized partial computation
- Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages
- Distributing the workload in a lazy theorem-prover
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Fast approximations of quantifier elimination
- An efficient SMT solver for string constraints
- Combining sets with cardinals
- Satisfiability Procedures for Combination of Theories Sharing Integer Offsets
- Combining equational reasoning
- Towards an integration science. The influence of Richard Bellman on our research.
- Combination of uniform interpolants via Beth definability
- Polite combination of algebraic datatypes
- Combination techniques and decision problems for disunification
- scientific article; zbMATH DE number 7533356 (Why is no real title available?)
- 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
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)
