A Practical Decision Procedure for Arithmetic with Function Symbols
From MaRDI portal
Cited in
(22)- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Combination of constraint solvers for free and quasi-free structures
- Complexity, convexity and combinations of theories
- An overview of the Tecton proof system
- Automatic synthesis of logical models for order-sorted first-order theories
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- Polite combination of algebraic datatypes
- Politeness for the theory of algebraic datatypes
- Milestones from the Pure Lisp Theorem Prover to ACL2
- Politeness and combination methods for theories with bridging functions
- Decidable cases of first-order temporal logic with functions
- A taxonomy of exact methods for partial Max-SAT
- Properties of a predicate transformer of the VRS system
- Predicate transformers in the context of symbolic modeling of transition systems
- Colors Make Theories Hard
- Problem-oriented program verification system ?SPEKTR?
- Elimination Techniques for Program Analysis
- Analyzing automata with Presburger arithmetic and uninterpreted function symbols
- Conditional rewrite rule systems with built-in arithmetic and induction
- Spectra and satisfiability for logics with successor and a unary function
- Str\(\dotplus\)ve and integers
This page was built for publication: A Practical Decision Procedure for Arithmetic with Function Symbols
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3960818)
