ICCL International Workshop
Deep Inference and Proof Theory 2005
Technische Universität Dresden
December 14-15, 2005

Please note that the dates of the workshop have changed (previously it was scheduled on 15-16th of December).


This meeting is dedicated to deep inference and related matters. The meeting will take place on December 14 and 15.

Participants

Talks

The Deep Inferential Aspects of the CORE Calculus
Serge Autexier

We present the CORE calculus for contextual reasoning which supports reasoning directly on the assertion level, where proof steps are justified in terms of applications of definitions, lemmas, theorems, or hypotheses (collectively called ``assertions'') and which is an established basis to generate proof presentations in natural language. The calculus is in the Deep Inference paradigm and comprises a uniform notion of a logical context of subformulas as well as replacement rules available in a logical context. Replacement rules operationalize assertion level proof steps and technically are generalized resolution and paramodulation rules, which in turn should suit the implementation of automatic reasoning procedures.

Yet another Proof Theory for Modal Logic
Kai Brünnler

There are many ways of giving cut-free axiomatisations for modal logic, but each of them has certain drawbacks. The general picture is that the richer the set of structural connectives of a certain formalism, the more modal logics this formalism captures systematically. Now, on one hand we want "generality", i.e. capture many logics, but on the other hand we also want a certain "purity" namely a structural level which is as small and simple as possible. Clearly, the more we allow at the structural level, the less meaningful the subformula property becomes. Three prominent formalisms, along the axis from general-and-not-so-pure to not-so-general-but-pure are the following: labelled systems, the display calculus and hypersequents. Recent work by Stewart/Stouppa on modal logic in the calculus of structures provides a fourth formalism which is as pure and at least as general as hypersequents, and more systematic. Stewart/Stouppa also conjecture it to be strictly more general than hypersequents. I apologise for adding yet another formalism to the zoo. It is based on deep inference and maintains the good properties both of hypersequents (i.e. the real subformula property) and the calculus of structures (systematicity) and gives us cut-free systems for strictly more logics (e.g. B and K5). These systems should be easy to embed into the calculus of structures in order to prove Stewart/Stouppa's conjecture and might also be a bit interesting on their own.

Models of Monad-Independent Dynamic Logic
Sergey Goncharov

Wired Deduction
Alessio Guglielmi

In order to get rid of bureaucracy in proofs, we might be bold and 1) abandon formulae for a special kind of labeled collapsible graphs, called relation webs; 2) build derivations out of the same constructors used for formulae; 3) allow inference rules to act on entire derivations and not just on formulae. By doing this we can design a formalism, called wired deduction, where many kinds of proof bureaucracy are absent. It is possible to express deep inference deductive systems in wired deduction without any use of equations, and without increasing the number and complexity of inference rules. Since this is not trivial, it looks interesting enough to justify the sacrifices mentioned above.

Nondeterminism in the Deep Inference Presentation of Classical Logic
Ozan Kahramanoğullari

Unlike the sequent calculus presentations, deep inference presentation of classical logic polynomially simulates popular proof procedures such as resolution. However, applicability of the inference rules at any depth causes greater nondeterminism than in the sequent calculus regarding proof search: in a bottom-up rule application in proof search, there are many more possible premises of a structure, however only a few of these instances provide a proof. Although deep inference provides much shorter proofs than, for example, in the sequent calculus, this wild nondeterminism is a drawback for applications. In this talk, I am going to discuss the proof theory of a technique for reducing nondeterminism in classical logic, and speculate about its potential applications.

Denotational Semantics for Classical Logic
François Lamarche

We wil present models of Classical Logic that are variations on Girard's coherence spaces, which gave birth to Linear Logic. An important intermediary step in our construction is getting models of Linear Logic with the Medial rule. The next hurdle is getting interesting classes of bimonoids in that linear category. Finally, we have to restrict the class of bimonoids so that a useable notion of map can be found, in which formal isos are really isomorphisms of bimonoids. Some of the categories we construct will also have additives, for Classical Logic.

Dial M for Monoidality
Richard McKinley

We discuss the connection between monoidality of functors on a categorical model of classical logic and the medial rule(s) of the calculus of structures.

Virtual Propositions: A Sequent Calculus for Medial Logic
Richard McKinley

By restricting the structual rules in a sequent calculus, we derive a calculus with weakening for a logic without weakening, in which the medial rule of the calculus of structures can be derived.

On the Role of Medial in a Boolean Category
Lutz Strassburger

In its most general meaning, a Boolean category is to categories what a Boolean algebra is to posets. In a more specific meaning a Boolean category should provide the abstract algebraic structure underlying the proofs in Boolean Logic, in the same sense as a Cartesian closed category captures the proofs in intuitionistic logic and a *-autonomous category captures the proofs in linear logic. However, recent work has shown that there is no canonical axiomatisation of a Boolean category. In this work, we will see a series (with increasing strength) of possible such axiomatisations, all based on the notion of *-autonomous category. We will particularly focus on the medial map, which has its origin in an inference rule in KS, a cut-free deductive system for Boolean logic in the calculus of structures.

Timetable

Wednesday 14.12 afternoon

Thursday 15.12 morning

Thursday 15.12 afternoon


Venue

Wednesday: Room 233 (Ratszimmer)
Thursday : Room 151
Computer Science Department
Hans-Grundig-Str. 25
01307 Dresden
Tel.: +49 (351) 463 38340 (Sylvia Epp, secretary)


8.12.2005 Ozan Kahramanoğullari Robert Hein