A Decision Procedure for the First Order Theory of Real Addition with Order

Cited In (73)

On the complexity of quantified linear systems
Complexity analysis of a unifying algorithm for model checking interval temporal logic
Symbolic model checking of timed guarded commands using difference decision diagrams
Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
Tractability conditions for numeric CSPs
Some new results on decidability for elementary algebra and geometry
Survey on mining signal temporal logic specifications
Łukasiewicz games: a logic-based approach to quantitative strategic interactions
Constraint satisfaction and semilinear expansions of addition over the rationals and the reals
Rank functions of tropical matrices
A bibliography of quantifier elimination for real closed fields
On time-space classes and their relation to the theory of real addition
Real addition and the polynomial hierarchy
An efficient decision procedure for the theory of rational order
The complexity of logical theories
A technique for proving decidability of containment and equivalence of linear constraint queries
Solving Łukasiewicz \(\mu\)-terms
Syntax-guided quantifier instantiation
On the complexity of model checking for syntactically maximal fragments of the interval temporal logic HS with regular expressions
MAX-closed semilinear constraint satisfaction
First-order logic and numeration systems
Model checking interval temporal logics with regular expressions
Tropically convex constraint satisfaction
Reachability relations of timed pushdown automata
On the decidability of semilinearity for semialgebraic sets and its implications for spatial databases
Circuit satisfiability and constraint satisfaction around Skolem arithmetic
Tropical semimodules of dimension two
Reasoning about negligibility and proximity in the set of all hyperreals
Ehrenfeucht-Fraïssé goes automatic for real addition
Proof synthesis and reflection for linear arithmetic
An exact correspondence of linear problems and randomizing linear algorithms
The complexity of query evaluation in indefinite temporal constraint databases
Don't care words with an application to the automata-based approach for real addition
Typechecking top-down XML transformations: Fixed input or output schemas
Constraint satisfaction problems over numeric domains
The complexity of one-agent refinement modal logic
Complexity of Boolean algebras
On reachability for hybrid automata over bounded time
Verification of Hybrid Systems
The complexity of almost linear diophantine problems
A tool for deciding the satisfiability of continuous-time metric temporal logic
A survey of satisfiability modulo theory
The complexity of tropical matrix factorization
The complexity of Presburger arithmetic with bounded quantifier alternation depth
The theory of integer multiplication with order restricted to primes is decidable
The complexity of one-agent refinement modal logic
A layered algorithm for quantifier elimination from linear modular constraints
Classifying the computational complexity of problems
Emptiness problems for integer circuits
Emptiness problems for integer circuits
LTL over integer periodicity constraints
Weak quantifier elimination for the full linear theory of the integers
An analogue of Cobham's theorem for graph directed iterated function systems
The complexity of linear problems in fields
Analyzing restricted fragments of the theory of linear arithmetic
A complete and terminating approach to linear integer solving
Exact complexity bounds for ordinal addition
Ehrenfeucht games and ordinal addition
Decidability of Definability Issues in the Theory of Real Addition
Linear quantifier elimination
Realizability modulo theories
Title not available (Why is that?)
Title not available (Why is that?)
SLAP: specification logic of actions with probability
Büchi automata recognizing sets of reals definable in first-order logic with addition and order
Erratum to: ``Analyzing restricted fragments of the theory of linear arithmetic
Title not available (Why is that?)
Taming strategy logic: non-recurrent fragments
Geometric decision procedures and the VC dimension of linear arithmetic theories
Timed Basic Parallel Processes
Łukasiewicz logics for cooperative games
Flow games
Double-exponential inseparability of Robinson subsystem \(Q_{+}\)

This page was built for publication: A Decision Procedure for the First Order Theory of Real Addition with Order

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4046035)