- N. Arai (Hiroshima)
- Title: Cut-free LK Quasi-Polynomially Simulates Resolution
Abstract:
In this talk, the relative efficiency of two propositional systems is
studied:
resolution and cut-free LK in DAG. We give an upper bound for translation of
resolution refutation to cut-free LK proofs. The best upper bound known was
$2^n$ and we improve it to $n^{2+3\log n}$.
- J. Avigad (Pittsburgh)
- Title: Interpreting classical theories in constructive ones
Abstract:
In this talk I will discuss a surprisingly uniform method of
interpreting a number of classical theories in constructive theories
having the same proof-theoretic strength. The classical theories
considered range in strength from bounded fragments of arithmetic to
Kripke-Platek admissible set theory.
- A. Beckmann (Münster)
- Title:
Dynamic ordinal analysis
- a tool for separating fragments of bounded arithmetic
Abstract:
We define the dynamic ordinal of a theory which is a suitable
analogue
of the usual prooftheoretic ordinal for weak theories of arithmetic. We
compute the dymanic ordinal of certain fragments of bounded arithmetic
by adapting methods from the Schütte-style ordinal analysis of the
fragments $I\Sigma^0_n$ of Peano-arithmetic. Then different dynamic
ordinals
immediately imply the separation of the associated fragments of bounded
arithmetic.
This way we also investigate very weak fragments of bounded
arithmetic based on induction for $s\Sigma^{bb}_n$-formulas.
The $s\Sigma^{bb}_n$-formulas
are build up from double sharply bounded formulas by counting
alternations of bounded quantifiers.
- S. Bellantoni (Toronto)
- Title: Ramification Today
Abstract:
This presentation will survey recent results in ramification and
complexity theory, in both the functional and logical settings.
Recent work has shown that ramification is an important tool in
controlling the computational complexity of subrecursive and
arithmetic systems. Another important tool in restricting
computational complexity is linearity, which is particularly useful
at higher type levels. The two can be integrated using mechanisms
from modal logic. The use of modality allows one to generalize the
concept of "ramification level" from ground type to all higher
types. Thus, for a type (sigma -> tau) one defines a corresponding
"complete" type !(sigma -> tau) at one higher ramification level.
Analogous to the modal axiom of distribution, in the functional
setting one has a term of type !(sigma -> tau) -> !sigma -> !tau.
- U. Berger (München
- Title: Normalization by Evaluation
- M. L. Bonet (Barcelona)
- Title: Automatization and non-Automatization
of Propositional Proof Systems
Abstract:
A propositional proof system S is automatizable if there is a deterministic
procedure that takes as input a formula and returns an S-refutation of it
(if one exists) in polynomial time in the size of the shortest S-refutation
of the formula. In the talk we will give an overview of what is known
about different proof systems, which are automatizable and which are not,
and which it is open if they are automatizable. The talk will contain some
recent results, but it will also be an overview of the topic.
- W. Burr (Münster)
- Title: Functional Interpretation
of Aczel's Constructive Set Theory CZF
Abstract:
We give a functional interpretation of Aczel's constructive set theories
CZF- and CZF in systems of constructive set functionals of finite types.
This interpretation is obtained by a new translation, a refinement of the
translation introduced by Diller and Nahm which again is an extension of
Gödel's Dialectica translation. The interpretation theorem gives
characterizations of the definable set functions of CZF- and CZF in terms
of constructive set functionals. In a second part we introduce constructive
set theories in all finite types. We expand the interpretation to these
theories and give a characterization of the new translation. Finally we show
that the simplest non-trivial axiom of extensionality (for type 2) is
not interpretable with constructive set-functionals.
We obtain this result by adapting Howard's notion of hereditarily
majorizable functionals to set functionals.
- H. de Nivelle (Amsterdam)
- Title: Deciding the E+ class with an a posteriori order
Abstract:
The talk is about resolution decision procedures.
A resolution decision procedure is a restriction of the
general resolution rule which is complete and which enforces
termination of the search process for some class of first order
formulae. (or a class of clause sets)
The E+ class is the basic class that has been
shown decidable by resolution. The restriction used
for the E+ class forms the basis for the decision techniques for
most other classes.
The technique used is an order <v which prefers those
literals containing the deepest occurrence of a variable.
This order is applied before the computation of the most general
unifier. (a priori)
This <v order is not preserved by substitution, which
makes it incompatible with subsumption.
I will show that the E+ class can be decided by a different
order, <vd, when this order is applied after the most general
unifier, i.e. a posteriori. The order <vd is preserved under
substitution. This makes the restriction compatible with full
subsumption.
This type of work fits well into a workshop on proof theory
because the techniques used allow proof theoretic proofs of
decidability results.
which before had only model theoretic proofs.
- R. Dyckhoff (St. Andrews)
- Title:
Contraction-free and permutation-free calculi for some non-classical logics
Abstract:
I shall discuss two kinds of sequent calculus: "contraction-free" calculi
and "permutation-free" calculi, emphasising the former's suitability for
solving decision problems and the latter's suitability for proof search (as
in logic programming).
The former have been investigated by Hudelmaier, myself and several others;
we report mainly on recent work (joint with Sara Negri) showing how their
completeness may (in some cases) be proven by rather routine methods
allowing extension with quantifiers or non-logical notions like apartness.
An example is given, however, of a terminating contraction-free calculus
for (propositional) Dummett logic, with all rules invertible, where less
routine methods still seem preferable.
The latter are based on work of Herbelin, and have the property that the
proofs are in 1-1 correspondence with normal natural deductions. We
discuss some recent work (joint with Luis Pinto) extending the ideas to
dependent type theory.
- S. Feferman (Stanford)
- Title: Unfolding Schematic Formal Systems
Abstract:
The unfolding of schematic formal systems is a novel concept which weds:
(i) functional (least fixed point) schemata for recursion over arbitrary
structures, to (ii) schematic formal systems S considered in a wider, more
open-ended sense than is customary in current metamathematics. The
concept of unfolding is used to answer the following general question:
*What operations, predicates and principles concerning them are implicit
in the acceptance of a given schematic system S?*
I will report on joint work with Thomas Strahm characterizing the
notion(s) of unfolding for non-finitist arithmetic, and then will explain
work in progress on this concept ranging from feasible and
finitist arithmetic to higher set theory.
- A. Hendriks (Amsterdam)
- Title: Doing logic by computer
Abstract:
This talk will be about computer experiments in (modal and intuitionistic)
propositional logic.
Some applications will be discussed of an approach to investigate questions in
logic using both theorem provers and computations in Kripke models.
One of the applications yields a counterexample to the interpolation
property for intuitionistic propositional logic with equivalence as the only
connective.
- M. Hofmann (Edinburgh)
- Title:
Extending "safe recursion" to higher types, lists, trees, and
polymorphism
Abstract:
Bellantoni-Cook's function system of "safe recursion"
is a first-order system which defines exactly the PTIME functions in
a "resource free" way by imposing a certain syntactic restriction on
primitive recursion on notation. We extend this idea to a typed lambda
calculus with lists, trees, and polymorphism. The syntactic
restriction contained in the Bellantoni-Cook approach is captured by
way of an S4 modality on types. The presence of trees and higher-typed
functions further introduces the need for linearity (in the sense of
linear logic) in certain places. The proof that the resulting calculus
defines PTIME functions only proceeds by a semantic interpretation
using realisability and functor categories.
The ultimate goal of this work is a realistic programming language for
polynomial time. Time permitting, I will also talk about some of the
obstacles which are yet to be overcome on the way.
- J. Johannsen (San Diego)
- Title:
Exponential Separations between Restricted Resolution and Cutting Planes
Proof Systems
Abstract:
This talk reports joint work with M.L. Bonet, J.L. Esteban and N. Galesi.
We prove an exponential lower bound for tree-like Cutting Planes refutations
of a set of clauses which has polynomial size resolution refutations. This
implies an exponential separation between tree-like and dag-like proofs for
both Cutting Planes and resolution; in both cases only superpolynomial
separations were known before.
In order to prove the lower bound, the lower bounds on the depth of monotone
circuits of Raz and McKenzie (FOCS 97) are extended to monotone real circuits.
In the case of resolution, this result is further improved by giving an
exponential separation of tree-like resolution from (dag-like) regular
resolution proofs. In fact, the refutation provided to give the upper bound
respects the stronger restriction of being a Davis-Putnam resolution proof.
Finally, we prove an exponential separation between Davis-Putnam resolution
and unrestricted resolution proofs; only a superpolynomial separation was
previously known.
- G. Mints (Stanford)
- Title: Reductions of finite and infinite proofs
Abstract:
Standard expansion of a finite proof d in arithmetic into an
infinite proof h(d) provides normalization theorems for finite proofs
of simple formulas, usually of complexity at most Sigma_1. A slight
modification of this expansion allows to normalize finite proofs of
arbitrary formulas, even if the normal form contains eigenvariables.
This approach extends to subsystems of analysis.
It can be used to extract a set of reductions for finite
proofs from cut-elimination for infinite proofs.
- I. Moerdijk (Utrecht)
- Title: Martin-Löf type theory and realisability
Abstract:
We discuss "internal" models of Martin-Löf type theory.
In particular, we show how to give an effective interpretation
of general inductive (W-)types within a predicative metatheory.
(Part of joint work with E. Palmgren, Uppsala).
- V. Orevkov (St. Petersburg)
- Title: The Complexity of Terms in Proofs
Abstract:
The aim of this talk is to obtain upper bounds on the complexity of
terms occurring in proofs in predicate calculus. We will consider Gentzen
sequential calculus both with cut and without cut. The bounds make possible
to compare lengths of direct and indirect proofs of existence theorems in
predicate calculus. Then we will extend our results to axiomatic theories
of algebraically closed and real-closed fields and to arithmetic without
multiplication.
- C. Pollett (Boston)
- Title: Multifunction Algebras and Provability of the Collapse of PH
Abstract:
In this talk I will introduce some multifunctions algebras which for i > 1
correspond to functions computable in polynomial time with a limited number of
witnessing queries to an oracle at the i-1 level of the hierarchy.
We then consider two subtheories of the well-studied bounded arithmetic theory
S_2 of Buss. Actually, one of our theories is contained in the other.
Using our algebras (mainly the i=1 variants on our algebras) we establish the
following properties for these theories:
- Neither theory can prove the polynomial hierarchy collapses.
- If either theory is contained in S^i_2 for some i then the polynomial
hierarchy collapses.
- If either theory proves the polynomial hierarchy is infinite then for all i,
S^i_2 can separate the ith level of the hierarchy.
- There is an interesting initial segment of any model of the weaker theory
that satisfies all of IDelta_0 + exp.
- A. A. Razborov (Moscow)
- Title: Lower Bounds for Algebraic Proof Systems
Abstract:
Algebraic proof systems are proof systems that operate with
(commutative) multi-variable polynomials over some ring and prove facts
of the form ``every solution to some system of polynomial equations is also a solution to another equation''. In this talk we are specifically interested in the combinatorial framework in which we by default include into the
set of axioms all equations $x^2-x=0$ ($x$ a variable; this ensures that we
are in the Boolean world), and pay a special attention to those facts
that reflect natural combinatorial principles.
Algebraic proof systems originally emerged as a tool for proving
lower bounds in the propositional proof complexity; more specifically,
for attacking the system of constant-depth Frege proofs allowing also modular
gates modulo some prime $p$. It soon became clear, however, that the
importance of algebraic proof systems goes far beyond this particular task:
they provide natural and elegant models for studying (our way of thinking
about) the most basic algebraic facts and constructions.
In this talk we firstly survey various connections between algebraic
proof systems on the one hand, and such areas as propositional proof
systems or automatic theorem proving on the other. In particular, we
try to explain from the complexity perspective what makes algebraic
proof systems very unique for the automatic proof generation. Then we
survey lower bounds known for algebraic proof systems.
- H. Schwichtenberg (München)
- Title: Ramification, Modality,
and Linearity in Higher Type Recursion
Abstract:
It is shown how to restrict Gödel's system $T$ of
recursion in all higher types, so that the type level 1 section
consists of exactly the polynomial-time computable functions. The
characterization is obtained by a novel combination of ramification
and linearity, which are made to coincide through modal operations
(joint work with S. Bellantoni and K.-H. Niggl).
- D. Scott (Pittsburgh)
- Title: Types and Computability
Abstract:
Over the last year, we have been developing a circle of ideas that
came up in Scott's 1996 graduate course on domain theory. The aim is
to use type theory (and topos theory) via realizability to model a
constructive logic which accomodates standard types (e.g. countably
based topological spaces) and domain theory (as certain countably
based T0-spaces), has extensive closure conditions
(e.g. as a cartesian closed and locally cartesian closed category),
and supports polymorphism (in the style of Girard and Reynolds or the
calculus of constructions).
Similar approaches having some of these advantages have been suggested
many times before, but we now think better results can be achieved
using realizability over the graph model for the (untyped) lambda
calculus. Moreover, in this proposed interpretation, there is a
clear-cut definition of a type operator #A, meaning the
formation of the computable elements of the type A (which
includes computable functions as a type #(A -> B)). This
operator can also be applied to propositions providing a constructive
version of an kind of S4 modal logic. In this way it is
possible for example to work both with the whole set of real numbers
along with the computable numbers and functions.
The major task of the project is to show that this logic is capable
of naturally formulating the constructions and proofs required for the
questions of semantics of programming languages - especially in
justifying the existence and properties of recursively defined types.
If this is successful, there should be significant conclusions for
constructuve logic as well.
- T. Strahm (Bern)
- Title: Abstract computations in type-free applicative systems
Abstract:
Type-free applicative theories build the operational basis
of Feferman's explicit mathematics. In this talk we survey
proof-theoretic aspects of various forms of abstract
computation in a type-free applicative setting. In particular,
we are interested in several type 2 functionals including
the Suslin operator E_1, Kleene's E and an operator
related to the polynomial time hierarchy. Thus we discuss
applicative systems ranging in proof-theoretic strength
from Delta-1-2 comprehension, predicative subsystems
of analysis to systems of feasible and bounded arithmetic.
- G. Takeuti (Philadelphia)
- Title: Forcing and P=/=NP
Abstract:
We discuss the forcing approach to P=/=NP problem.
- L. Trevisan (MIT)
- Title: Interactive and Probabilistic Proof-Checking
Abstract:
The informal statement that "proofs are easier to check than
to find" is the intuition on which the $P \neq NP$ conjecture
and much of Computational Complexity Theory are based.
In slightly more than a decade, the notion of "checking the validity
of a proof" has been stretched to unexpected limits, with
surprising and useful consequences that extend beyond the
limits of complexity theory.
The use of randomization and interaction in proof checking
(and, consequently, the notion of "probabilistically sound"
proof-systems) showed how to efficiently check proofs of
tautology-hood of propositional formulae, and even of
quantified propositional formulae.
Statements of such generality are conjectured not to have
short proofs in any reasonable proof system without interaction
and randomness, and it has been shown that they provably do
not have short proofs in certain standard proof systems such
as resolution.
Parallel to this developments, the counter-intuitive notion
of zero-knowledge proofs (proofs whose validity can be checked
with high confidence by a proof-checker that verifies
the validity of the proof without being able to replicate it
afterwards) was exploited, with general and powerful applications
to cryptographic protocols.
Probabilistically checkable proofs are the latest development
of this sort, with several applications to proving hardness of
approximation for fundamental optimization problems.
In our talk we will cover the sequence of ideas and techniques
that led to these results, and we will mention some interesting
open questions.
- J. van Oosten (Utrecht)
- Title: SDT in Modified Realizability
Abstract:
Synthetic Domain Theory (SDT) is the mathematical theory
that aims to find the most abstract form of axioms on
a category of "domains", so as to be able to perform the
standard constructions domain theory is usually used for:
semantics for programming languages, models for the
lambda calculus, etc.
It turns out that the axiomatization is most fruitfully
studied in an intuitionistic context, where nontrivial models
are available. The talk will present joint work with
Alex Simpson from Edinburgh, on models of SDT in the
Modified Realizability Topos. Interesting counterexamples
will be exhibited.
|