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

Cited in

(76)

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

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)