Filter by type:

A Characterisation of Definable NP Search Problems in Peano Arithmetic

conference
Arnold Beckmann
Logic, Language, Information and Computation. 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009. Pages: 1 - 12
Publication year: 2009

The complexity class of $\prec$-bounded local search problems with goals is introduced for well-orderings $\prec$, and is used to give a characterisation of definable NP search problems in Peano Arithmetic.

On the computational complexity of cut-reduction

conference
Klaus T Aehlig and Arnold Beckmann
Logic in Computer Science, 2008. LICS '08. 23rd Annual IEEE Symposium on 24-27 June 2008. Pages: 284 - 293
Publication year: 2008

Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations, and explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.

On the complexity of parity games

conference
Arnold Beckmann and Faron G Moller
Visions of Computer Science — BCS International Academic Conference Imperial College, London, UK - 22 - 24 September 2008. Pages: 237 - 247
Publication year: 2008

Parity games underlie the model checking problem for the modal μ-calculus, the complexity of which remains unresolved after more than two decades of intensive research. The community is split into those who believe this problem – which is known to be both in NP and coNP – has a polynomial-time solution (without the assumption that P=NP) and those who believe that it does not. (A third, pessimistic, faction believes that the answer to this question will remain unknown in their lifetime.)

In this paper we explore the possibility of employing Bounded Arithmetic to resolve this question, motivated by the fact that problems which are both NP and coNP, and where the equivalence between their NP and coNP description can be formulated and proved within a certain fragment of Bounded Arithmetic, necessarily admit a polynomial-time solution. While the problem remains unresolved by this paper, we do proposed another approach, and at the very least provide a modest refinement to the complexity of parity games (and in turn the μ-calculus model checking problem): that they lie in the class of Polynomial Local Search problems. This result is based on a new proof of memoryless determinacy which can be formalised in Bounded Arithmetic.

The approach we propose may offer a route to a polynomial-time solution. Alternatively, there may be scope in devising a reduction between the problem and some other problem which is hard with respect to PLS, thus making the discovery of a polynomial-time solution unlikely according to current wisdom.

Logic and Theory of Algorithms

edited volumes
Arnold Beckmann, Costas Dimitracopoulos, Benedikt Löwe
Fourth Conference on Computability in Europe, CiE 2008, Athens, Greece, June 2008, Proceedings, LNCS 5028
Publication year: 2008

From Gödel to Einstein: Computability between Logic and Physics at CiE 2006

special issues
Arnold Beckmann, Edwin Beggs, Benedikt Löwe
special issue of the journal Theoretical Computer Science A, Volume 394, Issue 3
Publication year: 2008

Continuous Fraïssé Conjecture

journal
Arnold Beckmann, Martin Goldstern and Norbert Preining
Order 2008, 25: 281-298
Publication year: 2008

We investigate the relation of countable closed linear orderings with respect to continuous monotone embeddability and show that there are exactly ℵ1 many equivalence classes with respect to this embeddability relation. This is an extension of Laver’s result, who considered (plain) embeddability, which yields coarser equivalence classes. Using this result we show that there are only ℵ0 many different Gödel logics.

Computability in Europe 2006

special issues
Arnold Beckmann, Benedikt Löwe
special issue of the journal Theory of Computing Systems, Volume 43, Issue 3-4
Publication year: 2008

Propositional Logic for Circuit Classes

conference
Klaus T Aehlig and Arnold Beckmann
21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Pages: 512 - 526
Publication year: 2007

By introducing a parallel extension rule that is aware of independence of the introduced extension variables, a calculus for quantified propositional logic is obtained where heights of derivations correspond to heights of appropriate circuits. Adding an uninterpreted predicate on bit-strings (analog to an oracle in relativised complexity classes) this statement can be made precise in the sense that the height of the most shallow proof that a circuit can be evaluated is, up to an additive constant, the height of that circuit.

The main tool for showing lower bounds on proof heights is a variant of an iteration principle studied by Takeuti. This reformulation might be of independent interest, as it allows for polynomial size formulae in the relativised language that require proofs of exponential height.

Logical Approaches to Computational Barriers: CiE 2006

special issues
Arnold Beckmann, Benedikt Löwe, Dag Normann
special issue of the journal Journal of Logic and Computation, Volume 17, Issue 6.
Publication year: 2007

Linear Kripke Frames and Gödel Logics

journal
Arnold Beckmann and Norbert Preining
The Journal of Symbolic Logic Vol. 72, No. 1, pp. 26-44
Publication year: 2007

We investigate the relation between logics of countable linear Kripke frames with constant domains and Gödel logics. We show that for any such Kripke frame there is a Gödel logic which coincides with the logic of this Kripke frame and vice versa. This allows us to transfer several recent results on Gödel logics to the logics of countable linear Kripke frames with constant domains.

Logical Approaches to Computational Barriers

edited volumes
Arnold Beckmann, Ulrich Berger, Benedikt Löwe, John V. Tucker
Second Conference on Computability in Europe, CiE 2006, Swansea, UK, July 2006, Proceedings, LNCS 3988
Publication year: 2006

Generalised dynamic ordinals - universal measures for implicit computational complexity

journal
Arnold Beckmann
Logic Colloquium '02, Lecture Notes in Logic 27: 48-74, Association for Symbolic Logic, La Jolla, CA, 2006.
Publication year: 2006

We extend the definition of dynamic ordinals to generalised dynamic ordinals. We compute generalised dynamic ordinals of all fragments of relativised bounded arithmetic by utilising methods from Boolean complexity theory, similar to [Krajicek1994]. We indicate the role of generalised dynamic ordinals as universal measures for implicit computational complexity. I.e., we describe the connections between generalised dynamic ordinals and witness oracle Turing machines for bounded arithmetic theories. In particular, through the determination of generalised dynamic ordinals we re-obtain well-known independence results for relativised bounded arithmetic theories.

Uniform proof complexity

journal
Arnold Beckmann
Journal of Logic and Computation 2005, 15: 433-446
Publication year: 2005

We define the notion of the uniform reduct of a propositional proof system as the set of those bounded formulas in the language of Peano Arithmetic which have polynomial size proofs under the Paris-Wilkie-translation. With respect to the arithmetic complexity of uniform reducts, we show that uniform reducts are Π^0_1-hard and obviously in Σ^0_2. We also show under certain regularity conditions that each uniform reduct is closed under bounded generalisation; that in the case the language includes a symbol for exponentiation, a uniform reduct is closed under modus ponens if and only if it already contains all true bounded formulas; and that each uniform reduct contains all true Π^b_1(α)-formulas.

Separation results for the size of constant-depth propositional proofs

journal
Arnold Beckmann and Sam Buss
Annals of Pure and Applied Logic 2005, 136: 30-55
Publication year: 2005

This paper proves exponential separations between depth d-LK and depth (d+1/2)-LK for every d in 0, 1/2, 1, 1 1/2,… utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d-LK and depth (d+1)-LK for d in 0,1,2,… . We investigate the relationship between the sequence-size, tree-size and height of depth d-LK-derivations for d in 0, 1/2, 1, 1 1/2,… and describe transformations between them.

We define a general method to lift principles requiring exponential tree-size (d+1/2)-LK-refutations for d in 0,1,2,… to principles requiring exponential sequence-size d-LK-refutations, which will be described for the Ramsey principle and d=0. From this we also deduce width lower bounds for resolution refutations of the Ramsey principle.

Festschrift on the occasion of Wolfram Pohlers 60th birthday

special issues
Arnold Beckmann, Jeremy Avigad, Georg Moser
special issue of the journal Annals of Pure and Applied Logic, Volume 136, Issues 1-2, Pages 1-218
Publication year: 2005

An Unexpected Separation Result in Linearly Bounded Arithmetic

journal
Arnold Beckmann and Jan Johannsen
Math. Log. Quart. 2005, 51: 191-200
Publication year: 2005

The theories S^i_1(α) and T^i_1(α) are the analogues of Buss’ relativized bounded arithmetic theories in the language where every term is bounded by a polynomial, and thus all definable functions grow linearly in length. For every i , a Σ^b_i+1(α) – formula TOP^i(α), which expresses a form of the total ordering principle, is exhibited that is provable in S^i+1_1(α) , but unprovable in T^i_1(α). This is in contrast with the classical situation, where S^i+1_2 is conservative over T^i_2 w.r.t. Σ^b_i+1-sentences. The independence results are proved by translations into propositional logic, and using lower bounds for corresponding propositional proof systems.

Preservation theorems and restricted consistency statements in bounded arithmetic

journal
Arnold Beckmann
Ann.Pure.Appl.Logic 2004, 126: 255-280
Publication year: 2004

We define and study a new restricted consistency notion for bounded arithmetic theories T2j. It is the strongest ∀Π1b-statement over S21 provable in T2j, similar to Con(Gi) in Krajíček and Pudlák, (Z. Math. Logik Grundl. Math. 36 (1990) 29) or RCon(Ti1) in Krajı́ček and Takeuti (Ann. Math. Artificial Intelligence 6 (1992) 107). The advantage of our notion over the others is that can directly be used to construct models of T2j. We apply this by proving preservation theorems for theories of bounded arithmetic of the following well-known kind: The ∀Π1b-separation of bounded arithmetic theories S2i from T2j (1⩽i⩽j) is equivalent to the existence of a model of S2i which does not have a Δ0b-elementary extension to a model of T2j.

ESSLLI 2003 - Course Material II

edited volumes
Arnold Beckmann, Norbert Preining
Collegium Logicum Volume 6, KGS Wien, 2004, VIII+105pp, ISBN 3-901546-01-4.
Publication year: 2004

Ingo Lepper and Georg Moser: Why Ordinals are Good for You;
Heribert Vollmer: First-Order Logic with Groupoidal Quantifiers.

ESSLLI 2003 - Course Material I

edited volumes
Arnold Beckmann, Norbert Preining
Collegium Logicum Volume 5: ESSLLI 2003 - Course Material I; KGS Wien, 2004, VIII+143pp, ISBN 3-901546-00-6.
Publication year: 2004

Aarne Ranta: Grammatical Framework Tutorial;
Frank Richter and Manfred Sailer: Basic Concepts of Lexical Resource Semantics.

Bounded Arithmetic and Resolution-Based Proof Systems

book
Arnold Beckmann and Jan Johannsen
Collegium Logicum Volume 7, published by the Kurt Gödel Society
Publication year: 2004

This book is about two topics on the borderline between logic and complexity theory, and in particular about the connections between these. The first topic is Bounded Arithmetic, and the other is the complexity of propositional proof systems.

Ordinal Notations and Well-Orderings in Bounded Arithmetic

journal
Arnold Beckmann, Samuel R. Buss, Chris Pollett
Ann.Pur.Appl.Logic 2003, 120: 197-223
Publication year: 2003

Ordinal notations and provability of well-foundedness have been a central tool in the study of the consistency strength and computational strength of formal theories of arithmetic. This development began with Gentzen’s consistency proof for Peano arithmetic based on the well-foundedness of ordinal notations up to ε_0 . Since the work of Gentzen, ordinal notations and provable well-foundedness have been studied extensively for many other formal systems, some stronger and some weaker than Peano arithmetic. In the present paper, we investigate the provability and non-provability of well-foundedness of ordinal notations in very weak theories of bounded arithmetic, notably the theories S^i_2 and T^i_2 with 1 ≤ i ≤ 2 . We prove several results about the provability of well-foundedness for ordinal notations; our main results state that for the usual ordinal notations for ordinals below ε_0 and Γ_0, the theories T^i2 and S^2_2 can prove the ordinal Σ^b_1 – minimization principle over a bounded domain. PLS is the class of functions computed by a polynomial local search to minimize a cost function. It is a corollary of our theorems that the cost function can be allowed to take on ordinal values below Γ_0 , without increasing the class PLS .

Dynamic ordinal analysis

journal
Arnold Beckmann
Archive for Mathematical Logic Vol. 42, pp. 303-334
Publication year: 2003

Dynamic ordinal analysis is ordinal analysis for weak arithmetics like fragments of bounded arithmetic. In this paper we will define dynamic ordinals – they will be sets of number theoretic functions measuring the amount of Π^b_1(α) order induction available in a theory. We will compare order induction to successor induction over weak theories. We will compute dynamic ordinals of the bounded arithmetic theories Σ^b_n(α)-L^mIND for m=n and m=n+1, n≥0 . Different dynamic ordinals lead to separation. Therefore, we will obtain several separation results between these relativized theories. We will generalize our results to arbitrary languages extending the language of Peano arithmetic.

Resolution Refutations and Propositional Proofs with Height-Restrictions

conference
Arnold Beckmann
In: Bradfield J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg, Pages 599 - 612.
Publication year: 2002

Height restricted resolution (proofs or refutations) is a natural restriction of resolution where the height of the corresponding proof tree is bounded. Height restricted resolution does not distinguish between tree- and sequence-like proofs. We show that polylogarithmic-height resolution is strongly connected to the bounded arithmetic theory S^1_2(\alpha) . We separate polylogarithmic-height resolution from quasi-polynomial size tree-like resolution. Inspired by this we will study infinitely many sub-linear-height restrictions given by functions n → 2_i((log^(i+1) n)^O(1)) for i ≥ 0 . We show that the resulting resolution systems are connected to certain bounded arithmetic theories, and that they form a strict hierarchy of resolution proof systems. To this end we will develop some proof theory for height restricted proofs.

Proving consistency of equational theories in bounded arithmetic

journal
Arnold Beckmann
The Journal of Symbolic Logic Vol. 67, No. 1, pp. 279-296
Publication year: 2002

We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definition of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S^1_2 . In particular this solves an open problem formulated by Takeuti.

Notations for Exponentiation

journal
Arnold Beckmann
Theoretical Computer Science Vol. 288 No. 1, pp. 3-19
Publication year: 2002

We define a coding of natural numbers — which we will call the exponential notations — and interpretations of the less-than-relation, the successor function, addition and exponentiation on the exponential notations. We prove that all these interpretations are polynomial time computable. As an application we show that we can interpret terms over a certain restricted language — including exponentiation — in polynomial time on exponential notations.

A note on universal measures for weak implicit computational complexity

conference
Arnold Beckmann
9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Pages: 53 - 67
Publication year: 2002

This note is a case study for finding universal measures for weak implicit complexity. We will instanciate “universal measures” by “dynamic ordinals”, and “weak implicit complexity” by “bounded arithmetic”. Concretely, we will describe the connection between dynamic ordinals and witness oracle Turing machines for bounded arithmetic theories.

A non-well-founded primitive recursive tree provably well-founded for co-r.e. sets

journal
Arnold Beckmann
Archive for Mathematical Logic 2002, Vol. 41, No. 3, pp. 251-257
Publication year: 2002

We show that there is a primitive recursive tree which is not well-founded, but which is well-founded for co-r.e. sets, provable in Σ_1-Ind. It follows that the supremum of order-types of primitive recursive well-orderings, whose well-foundedness on co-r.e. sets is provable in Σ_1-Ind, equals the limit of all recursive ordinals.

Exact bounds for lengths of reductions in typed λ - calculus

journal
Arnold Beckmann
The Journal of Symbolic Logic Vol. 66, No. 3, pp. 1277-1285
Publication year: 2001

We determine the exact bounds for the length of an arbitrary reduction sequence of a term in the typed λ – calculus with β -, ξ – and η – conversion. There will be two essentially different classifications, one depending on the height and the degree of the term and the other depending on the length and the degree of the term.

Characterizing the elementary recursive functions by a fragment of Gödel's T

journal
Arnold Beckmann and Andreas Weiermann
Archive for Mathematical Logic, Volume 39, Issue 7, Pages 475-491.
Publication year: 2000

We use a modified Howard-Schütte-function [ ]_0 which assigns finite ordinals to each term from Tpred and which witnesses the strong normalization for T^pred . Furthermore the derivation lengths function for T^pred is elementary recursive, hence representable functions in T^pred are computable in elementary time, hence are elementary recursive. On the other hand it is shown that random-access machine transitions can be simulated in simple typed combinatorial calculus with combinators for the case distinction function and for the predecessor function, hence T^pred represents any elementary recursive function.

Analyzing Gödel's T via expanded head reduction trees

journal
Arnold Beckmann and Andreas Weiermann
Mathematical Logic Quarterly, Volume 46, Issue 4, Pages 517-536
Publication year: 2000

Inspired from Buchholz’ ordinal analysis of ID_1 and Beckmann’s analysis of the simple typed λ – calculus we classify the derivation lengths for Gödel’s system T in the λ – formulation (where the η – rule is included).