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

Cited in

(75)

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
Tractability conditions for numeric CSPs
Some new results on decidability for elementary algebra and geometry
Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
Survey on mining signal temporal logic specifications
Realizability modulo theories
Ł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
scientific article; zbMATH DE number 7577569 (Why is no real title available?)
On time-space classes and their relation to the theory of real addition
Real addition and the polynomial hierarchy
SLAP: specification logic of actions with probability
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
Model checking interval temporal logics with regular expressions
MAX-closed semilinear constraint satisfaction
Tropically convex constraint satisfaction
First-order logic and numeration systems
Reachability relations of timed pushdown automata
On the decidability of semilinearity for semialgebraic sets and its implications for spatial databases
Reasoning about negligibility and proximity in the set of all hyperreals
Circuit satisfiability and constraint satisfaction around Skolem arithmetic
Ehrenfeucht-Fraïssé goes automatic for real addition
Tropical semimodules of dimension two
Proof synthesis and reflection for linear arithmetic
Büchi automata recognizing sets of reals definable in first-order logic with addition and order
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
Erratum to: ``Analyzing restricted fragments of the theory of linear arithmetic
An exact correspondence of linear problems and randomizing linear algorithms
Typechecking top-down XML transformations: Fixed input or output schemas
The complexity of one-agent refinement modal logic
Proof theory of Riesz spaces and modal Riesz spaces
Complexity of Boolean algebras
Constraint satisfaction problems over numeric domains
On reachability for hybrid automata over bounded time
scientific article; zbMATH DE number 7379289 (Why is no real title available?)
Verification of Hybrid Systems
The adversarial Stackelberg value in quantitative games
The complexity of almost linear diophantine problems
A tool for deciding the satisfiability of continuous-time metric temporal logic
Taming strategy logic: non-recurrent fragments
A survey of satisfiability modulo theory
Duper: a proof-producing superposition theorem prover for dependent type 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
Geometric decision procedures and the VC dimension of linear arithmetic theories
Timed Basic Parallel Processes
Classifying the computational complexity of problems
Emptiness problems for integer circuits
LTL over integer periodicity constraints
Emptiness problems for integer circuits
Łukasiewicz logics for cooperative games
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
Flow games
Double-exponential inseparability of Robinson subsystem \(Q_{+}\)
A complete and terminating approach to linear integer solving
Exact complexity bounds for ordinal addition
Ehrenfeucht games and ordinal addition
Linear quantifier elimination
Decidability of Definability Issues in the Theory of Real Addition

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)