A Decision Procedure for the First Order Theory of Real Addition with Order
From MaRDI portal
Publication:4046035
DOI10.1137/0204006zbMath0294.02022OpenAlexW2021592352MaRDI QIDQ4046035
Jeanne Ferrante, Charles W. Rackoff
Publication date: 1975
Published in: SIAM Journal on Computing (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/6a7e0501315cbcaee5745d7b1082eea5c0f9d49c
Related Items (71)
Decidability of Definability Issues in the Theory of Real Addition ⋮ Łukasiewicz Games ⋮ Rank functions of tropical matrices ⋮ Constraint satisfaction and semilinear expansions of addition over the rationals and the reals ⋮ Complexity analysis of a unifying algorithm for model checking interval temporal logic ⋮ A layered algorithm for quantifier elimination from linear modular constraints ⋮ Erratum to: ``Analyzing restricted fragments of the theory of linear arithmetic ⋮ Reasoning about negligibility and proximity in the set of all hyperreals ⋮ Tropically convex constraint satisfaction ⋮ Verification of Hybrid Systems ⋮ The complexity of linear problems in fields ⋮ A bibliography of quantifier elimination for real closed fields ⋮ The Complexity of One-Agent Refinement Modal Logic ⋮ The complexity of query evaluation in indefinite temporal constraint databases ⋮ Ehrenfeucht games and ordinal addition ⋮ Circuit satisfiability and constraint satisfaction around Skolem arithmetic ⋮ Emptiness problems for integer circuits ⋮ Model checking interval temporal logics with regular expressions ⋮ On the complexity of quantified linear systems ⋮ Complexity of Boolean algebras ⋮ Taming strategy logic: non-recurrent fragments ⋮ Unnamed Item ⋮ Classifying the computational complexity of problems ⋮ Unnamed Item ⋮ On time-space classes and their relation to the theory of real addition ⋮ The theory of integer multiplication with order restricted to primes is decidable ⋮ The complexity of logical theories ⋮ First-Order Logic and Numeration Systems ⋮ Unnamed Item ⋮ The complexity of Presburger arithmetic with bounded quantifier alternation depth ⋮ The complexity of tropical matrix factorization ⋮ SLAP: specification logic of actions with probability ⋮ Büchi Automata Recognizing Sets of Reals Definable in First-Order Logic with Addition and Order ⋮ Reachability relations of timed pushdown automata ⋮ Constraint Satisfaction Problems over Numeric Domains ⋮ Typechecking top-down XML transformations: Fixed input or output schemas ⋮ Timed Basic Parallel Processes ⋮ Syntax-guided quantifier instantiation ⋮ Exact complexity bounds for ordinal addition ⋮ Weak quantifier elimination for the full linear theory of the integers ⋮ Proof synthesis and reflection for linear arithmetic ⋮ On Reachability for Hybrid Automata over Bounded Time ⋮ Analyzing restricted fragments of the theory of linear arithmetic ⋮ Solving Łukasiewicz \(\mu\)-terms ⋮ Tractability conditions for numeric CSPs ⋮ Max-Closed Semilinear Constraint Satisfaction ⋮ Linear quantifier elimination ⋮ Ehrenfeucht-Fraïssé goes automatic for real addition ⋮ Some new results on decidability for elementary algebra and geometry ⋮ LTL over integer periodicity constraints ⋮ Unnamed Item ⋮ An efficient decision procedure for the theory of rational order ⋮ Unnamed Item ⋮ The complexity of one-agent refinement modal logic ⋮ A technique for proving decidability of containment and equivalence of linear constraint queries ⋮ Double-exponential inseparability of Robinson subsystem Q+ ⋮ The complexity of almost linear diophantine problems ⋮ A complete and terminating approach to linear integer solving ⋮ Don't care words with an application to the automata-based approach for real addition ⋮ A Survey of Satisfiability Modulo Theory ⋮ Unnamed Item ⋮ Łukasiewicz logics for cooperative games ⋮ Emptiness Problems for Integer Circuits ⋮ An Exact Correspondence of Linear Problems and Randomizing Linear Algorithms ⋮ Tropical semimodules of dimension two ⋮ On the decidability of semilinearity for semialgebraic sets and its implications for spatial databases ⋮ Symbolic model checking of timed guarded commands using difference decision diagrams ⋮ An analogue of Cobham's theorem for graph directed iterated function systems ⋮ Real addition and the polynomial hierarchy ⋮ Survey on mining signal temporal logic specifications ⋮ A tool for deciding the satisfiability of continuous-time metric temporal logic
This page was built for publication: A Decision Procedure for the First Order Theory of Real Addition with Order
