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
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
