The computational complexity of logical theories

Publication date: 1979

Published in: Lecture Notes in Mathematics (Search for Journal in Brave)

Lower Bound Upper Bound Decision Procedure Pairing Functions Decidable Theories Computational Complexity of Logical Theories Efficient Arithmetization of Turing Machines Ehrenfeucht Games Equal Length Predicate Finite Abelian Groups First Order Theory Integers Lexicographical Order Monadic Predicate One Successor Real Numbers Two Successors Unary Function Well-Order

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Turing machines and related notions (03D10)

Related Items (84)

Sharpened lower bounds for cut elimination ⋮ On iterating linear transformations over recognizable sets of integers ⋮ On the complexity of decision using destinies in $H$-bounded structures ⋮ On the complexity of theories of permutations ⋮ Complexity of Subcases of Presburger Arithmetic ⋮ Nonconvergence, undecidability, and intractability in asymptotic problems ⋮ On the computational complexity of the theory of Abelian groups ⋮ The complexity of linear problems in fields ⋮ A bibliography of quantifier elimination for real closed fields ⋮ NP satisfiability for arrays as powers ⋮ Vaught's Theorem on Axiomatizability by a Scheme ⋮ Circuit Satisfiability and Constraint Satisfaction Around Skolem Arithmetic ⋮ Complexity of Presburger arithmetic with fixed quantifier dimension ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ The complexity of query evaluation in indefinite temporal constraint databases ⋮ Subclasses of Presburger arithmetic and the polynomial-time hierarchy ⋮ Dominoes and the complexity of subclasses of logical theories ⋮ Computational complexity of logical theories of one successor and another unary function ⋮ Quantifier elimination for the reals with a predicate for the powers of two ⋮ The most nonelementary theory ⋮ Algorithmic uses of the Feferman-Vaught theorem ⋮ Ehrenfeucht games and ordinal addition ⋮ Presburger Arithmetic, Rational Generating Functions, and Quasi-Polynomials ⋮ Short proofs for slow consistency ⋮ Circuit satisfiability and constraint satisfaction around Skolem arithmetic ⋮ Emptiness problems for integer circuits ⋮ Fixed point characterization of infinite behavior of finite-state systems ⋮ A small reflection principle for bounded arithmetic ⋮ Queries with arithmetical constraints ⋮ Finitely axiomatized theories lack self‐comprehension ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ On decidable varieties of Heyting algebras ⋮ The theory of hereditarily bounded sets ⋮ On Presburger arithmetic extended with non-unary counting quantifiers ⋮ Alternating complexity of counting first-order logic for the subword order ⋮ Locality and modular Ehrenfeucht-Fraïssé games ⋮ On algebraic array theories ⋮ Classifying the computational complexity of problems ⋮ 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 ⋮ A uniform method for proving lower bounds on the computational complexity of logical theories ⋮ The second incompleteness theorem and bounded interpretations ⋮ Definability with bounded number of bound variables ⋮ Skolem functions of arithmetical sentences. ⋮ Fast theorem-proving and Wu's method ⋮ Upper Bounds on the Automata Size for Integer and Mixed Real and Integer Linear Arithmetic (Extended Abstract) ⋮ Truth definition for $\Delta _ 0$ formulas and PSPACE computations ⋮ Pairs, sets and sequences in first-order theories ⋮ Weak quantifier elimination for the full linear theory of the integers ⋮ Knowledgebase transformations ⋮ An improved lower bound for the elementary theories of trees ⋮ A decision algorithm for linear sentences on a PFM ⋮ The unprovability of small inconsistency. A study of local and global interpretability ⋮ A closed-form evaluation for Datalog queries with integer (gap)-order constraints ⋮ Quantifier Elimination and Provers Integration ⋮ Complexity of logical theories involving coprimality ⋮ VON NEUMANN’S CONSISTENCY PROOF ⋮ Halting and Equivalence of Program Schemes in Models of Arbitrary Theories ⋮ Logical aspects of Cayley-graphs: the group case ⋮ Multitree automata that count ⋮ Decidability of the theory of the natural integers with the Cantor pairing function and the successor ⋮ Model-theoretic methods in combined constraint satisfiability ⋮ Unnamed Item ⋮ A Generalization of Semenov’s Theorem to Automata over Real Numbers ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Decidable ${\exists}^*{\forall}^*$ first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ An efficient decision procedure for the theory of rational order ⋮ The quantifier complexity of polynomial-size iterated definitions in first-order logic ⋮ Double-exponential inseparability of Robinson subsystem Q₊ ⋮ The complexity of almost linear diophantine problems ⋮ A complete and terminating approach to linear integer solving ⋮ Uniformly Automatic Classes of Finite Structures ⋮ Effective Quantifier Elimination for Presburger Arithmetic with Infinity ⋮ Model Checking FO(R) over One-Counter Processes and beyond ⋮ Emptiness Problems for Integer Circuits ⋮ The complexity of the word problems for commutative semigroups and polynomial ideals ⋮ Linear problems in valued fields ⋮ On the definability of properties of finite graphs ⋮ Turing machines with linear alternation, theories of bounded concatenation and the decision problem of first order theories ⋮ Strong reducibilities ⋮ Stationary logic of ordinals ⋮ New formally undecidable propositions: Non-trivial lower bounds on proof complexity and related theorems ⋮ Diophantine equations, Presburger arithmetic and finite automata

This page was built for publication: The computational complexity of logical theories