Catálogo de publicaciones - libros

Probably the most significant result concerning cut-free sequent calculus proofs in linear logic is the completeness of focused proofs. This completeness theorem has a number of proof theoretic applications — e.g. in game semantics, Ludics, and proof search — and more computer science applications — e.g. logic programming, call-by-name/value evaluation. Andreoli proved this theorem for first-order linear logic 15 years ago. In the present paper, we give a new proof of the completeness of focused proofs in terms of proof transformation. The proof of this theorem is simple and modular: it is first proved for MALL and then is extended to full linear logic. Given its modular structure, we show how the proof can be extended to larger systems, such as logics with induction. Our analysis of focused proofs will employ a proof transformation method that leads us to study how focusing and cut elimination interact. A key component of our proof is the construction of a which provides an abstraction over how focusing can be organized within a given cut-free proof. Using this graph abstraction allows us to provide a detailed study of atomic in a way more refined that is given in Andreoli’s original proof. Permitting more flexible assignment of bias will allow this completeness theorem to help establish the completeness of a number of other automated deduction procedures. Focalization graphs can be used to justify the introduction of an inference rule for derivation: a rule that should help us better understand the relations between sequentiality and concurrency in linear logic.

We define a notion of relational linear combinatory algebra (rLCA) which is a generalization of a linear combinatory algebra defined by Abramsky, Haghverdi and Scott. We also define a category of assemblies as well as a category of modest sets which are realized by rLCA. This is a linear style of realizability in a way that duplicating and discarding of realizers is allowed in a controlled way. Both categories form linear-non-linear models and their coKleisli categories have a natural number object. We construct some examples of rLCA’s which have some relations to well known PCA’s.

We provide a new correctness criterion for unit-free MLL proof structures and MELL proof structures with units. We prove that deciding the correctness of a MLL and of a MELL proof structure is -complete. We also prove that deciding the correctness of an intuitionistic multiplicative essential net is -complete.

A focused proof system provides a normal form to cut-free proofs that structures the application of invertible and non-invertible inference rules. The focused proof system of Andreoli for linear logic has been applied to both the and the approaches to computation. Various proof systems in literature exhibit characteristics of focusing to one degree or another. We present a new, focused proof system for intuitionistic logic, called , and show how other proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use to design a focused proof system for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard’s LC and LU proof systems.

We consider the problem of automating and checking the use of previously proved lemmas in the proof of some main theorem. In particular, we call the collection of such previously proved results a and use a partial order on the table’s entries to denote the (provability) dependency relationship between tabled items. Tables can be used in automated deduction to store previously proved subgoals and in interactive theorem proving to store a sequence of lemmas introduced by a user to direct the proof system towards some final theorem. Tables of literals can be incorporated into sequent calculus proofs using two ideas. First, cuts are used to incorporate tabled items into a proof: one premise of the cut requires a proof of the lemma and the other branch of the cut inserts the lemma into the set of assumptions. Second, to ensure that lemma is not reproved, we exploit the fact that in , atoms can have different . Using these ideas, simple logic engines that do focused proof search (such as logic programming interpreters) are able to check proofs for correctness with guarantees that previous work is not redone. We also discuss how a table can be seen as a proof object and discuss some possible uses of tables-as-proofs.

Sequent calculi usually provide a general deductive setting that uniformly embeds other proof-theoretical approaches, such as tableaux methods, resolution techniques, goal-directed proofs, etc. Unfortunately, in temporal logic, existing sequent calculi make use of a kind of inference rules that prevent the effective mechanization of temporal deduction in the general setting. In particular, temporal sequent calculi either need some form of cut, or they make use of invariants, or they include infinitary rules. This is the case even for the simplest kind of temporal logic, propositional linear temporal logic (PLTL). In this paper, we provide a complete finitary sequent calculus for PLTL, called , that not only is cut-free but also invariant-free. In particular, we introduce new rules which provide a new style of temporal deduction. We give a detailed proof of completeness.

In 1973, Parikh proved a speed-up theorem conjectured by Gödel 37 years before: there exist arithmetical formulæ that are provable in first order arithmetic, but whose shorter proof in second order arithmetic is arbitrarily smaller than any proof in first order. On the other hand, resolution for higher order logic can be simulated step by step in a first order narrowing and resolution method based on deduction modulo, whose paradigm is to separate deduction and computation to make proofs clearer and shorter.

We prove that  + 1-th order arithmetic can be linearly simulated into -th order arithmetic modulo some confluent and terminating rewrite system. We also show that there exists a speed-up between -th order arithmetic modulo this system and -th order arithmetic without modulo. All this allows us to prove that the speed-up conjectured by Gödel does not come from the deductive part of the proofs, but can be expressed as simple computation, therefore justifying the use of deduction modulo as an efficient first order setting simulating higher order.

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.

The Prover/Delayer game is a combinatorial game that can be used to prove upper and lower bounds on the size of Tree Resolution proofs, and also perfectly characterizes the space needed to compute them. As a proof system, Tree Resolution forms the underpinnings of all DPLL-based SAT solvers, so it is of interest not only to proof complexity researchers, but also to those in the area of propositional reasoning. In this paper, we prove the PSPACE-Completeness of the Prover/Delayer game as well as the problem of predicting Tree Resolution space requirements, where space is the number of clauses that must be kept in memory simultaneously during the computation of a refutation. Since in practice memory is often a limiting resource, researchers developing SAT solvers may wish to know ahead of time how much memory will be required for solving a certain formula, but the present result shows that predicting this is at least as hard as it would be to simply find a refutation.

We define strong monads of , and of , modeling both probabilistic and non-deterministic choice. This is an elegant alternative to recent proposals by Mislove, Tix, Keimel, and Plotkin. We show that our monads are sound and complete, in the sense that they model exactly the interaction between probabilistic and (demonic, angelic, chaotic) choice.