ABSTRACT. Abstract TBA

ABSTRACT. We begin with display and labelled calculi for a certain class of tense logics. These tense logics are extensions of Kt with any finite number of general path axioms, which are axioms of the form Xp -> Yp, where X and Y represent sequences of black and white diamonds.

For the minimal tense logic Kt, I provide a bi-directional embedding between display calculus proofs and labelled calculus proofs. It is then shown how to translate display proofs for Kt extended with general path axioms into labelled proofs.

Providing a reverse translation--translating labelled proofs into display proofs for Kt extended with general path axioms--has proven to be much more difficult because certain labelled structural rules do not correspond well to the display variants of such rules. Nevertheless, for a certain subclass of general path axioms a translation from labelled calculus proofs to display calculus proofs can be provided. Through the addition of special rules, referred to as "propagation rules," we can prove that the problematic structural rules are admissible in the resulting calculus. Every proof of a formula in this calculus contains sequents whose structure corresponds to a tree with two types of edges. This specific structure allows us to translate these proofs into display proofs, which gives an answer to an open question of translating labelled proofs to display proofs for extensions of the minimal tense logic Kt.

ABSTRACT. We propose a minimal non-normal intuitionistic modal logic. We present it by Hilbert axiomatisation and an equivalent cut-free calculus. We then propose a semantic characterisation of this logic in terms of bi-neighbourhood models with respect to which the logic is sound. We finally present a cut-free labelled calculus matching with the bi-neighbourhood semantics.

ABSTRACT. This paper provides the first proof-theoretic study of quantified non-normal modal logics. It introduces labelled sequent calculi for the first order extension, both with free and with classical quantification, of all the monotone non-normal modal logics, as well as of some interesting extensions thereof, and it studies the role of the Barcan Formulas in these calculi. It will be shown that the calculi introduced have good structural properties: they have invertibility of the rules, height-preserving admissibility of weakening and contraction, and syntactic cut elimination. It will also be shown that each of the calculi introduced is sound and complete with respect to the appropriate class of neighbourhood frames with either constant or varying domains. In particular the completeness proof constructs a formal proof for derivable sequents and a countermodel for underivable ones, and it gives a semantic proof of the admissibility of cut. Finally, some preliminay results on the extension of our approach to the non-monotonic case are discussed.

ABSTRACT. Multimodal logic has been studied for various purposes.
Although some studies have considered an infinite number of modalities,
propositions for the quantification of modalities, such as
``For all modalities [i] in an infinite set of modalities S, [i]p is true''
have not been discussed in general.
In this paper, a simple method for expressing these propositions is discussed and deduction systems for new logic are established.
The conditions on Kripke frames that include these notions are also discussed.

ABSTRACT. Logics arising from automaton theory, relational algebra and formal language theory are still not well understood in proof-theoretic terms. However, there is increasing evidence to suggest that emerging trends in structural proof theory, namely richer proof calculi and non-wellfounded proofs, possess the capacity to capture these fundamental frameworks, and even deliver important metalogical results of independent interest. In this talk I will speak about a recent line of work that uses a combination of internal calculi and cyclic proofs (arguably an external feature) to recover proof theoretic treatments for Kleene algebras (KA) and action lattices (AL).

Starting with KA, I show how a natural sound and complete non-wellfounded system can be made regular via enriching the syntax of proof lines to hypersequents. This takes advantage of several basic techniques on the cyclic proof side as well as known normal forms from automaton theory, morally corresponding to the use of hypersequents. This calculus exhibits optimal proof-search complexity and, as an application, I will briefly present work in progress on how to recover an alternative proof of the completeness of KA with respect to inclusions of rational languages. I will also speak about a proof theoretic account of AL, which is of natural interest to structural proof theorists since it extends the full Lambek calculus by a single fixed point: the Kleene star. The main result here is cut-elimination, which requires a sophisticated computational interpretation into a higher-order language. As an application we are able to recover an (optimal) complexity bound for *-continuous action lattices.

The aim of this talk is to give a concrete showcase of modern trends structural proof theory, and moreover to leave the audience with some motivational problems for the area at large. At a high-level, I also hope to explore a moral connection, in certain settings, between the richness of a proof calculus and succinct representations arising from automaton theory, which could direct a line of future research for the area.

ABSTRACT. In order to study proof translations in BI logic, we consider first the bunched sequent calculus LBI and then define a new labelled sequent calculus, called GBI. Therefore we propose a procedure that translates LBI proofs into GBI proofs and prove its soundness. Moreover we discuss some steps towards the reverse translation of GBI proofs into LBI proofs and propose an algorithm that is illustrated by some examples. Further work will be devoted to its proof of correctness and also to the design of translations of LBI proofs to TBI (labelled-tableaux) proofs.

ABSTRACT. We outline a proof-theoretic approach to the semantics of intensional operators for intuitionistic belief and knowledge, which does neither intend to capture a given target modal logic, nor to import ideas from relational model-theoretic semantics (e.g., truth at indices, accessibility between indices) via labelled and relational formulae into the language. On this approach, the meaning of these intensional operators is explained exclusively by appeal to the structure of proofs which are unaided by such means. The proof-theoretic framework chosen for this purpose is subatomic natural deduction proposed by the author in earlier work. The resulting systems normalize and enjoy the subexpression property (a refinement of the subformula property). They can be used for the logical analysis of reasoning patterns which involve complex multi-agent belief constructions (e.g., reciprocating or universal beliefs).

ABSTRACT. The logic of Conditional Beliefs (CDL) has been introduced by Board, Baltag and Smets to reason about knowledge and revisable beliefs in a multi-agent setting. Our aim is to develop standard internal calculi for this logic. As a preliminary result we propose an internal hypersequent calculus for it in the single agent case.

ABSTRACT. The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. Here we apply this method to derive the unprovability of a goal formula G in Intuitionistic Propositional Logic. To this aim we design a forward calculus FRJ(G) for Intuitionistic unprovability which is prone to constructively ascertain the unprovability of a formula G by providing a concise countermodel for it; in particular we prove that the generated countermodels have minimal height. Moreover, we clarify the role of the saturated database obtained as result of a failed proof-search in FRJ(G) by showing how to extract from such a database a derivation witnessing the Intuitionistic validity of the goal.