Workshop

General Information

A one day workshop on External and Internal Calculi for Non-Classical Logics will be held the 19 July 2018 in conjunction with IJCAR 2018 during FLOC 2018.

A special issue of a Journal is expected on these topics, with a deadline for submission of approximately 3 or 4 months after the workshop.

Scope

The widespread application of logical methods in several areas of computer science, epistemology and artificial intelligence has resulted in an explosion of new logics. These logics are more expressive than classical logic, allowing finer distinctions and a direct representation of notions that cannot be well stated in classical logic. For instance they are used to express different modes of truth (modal logics) and to study different types of reasoning, like reasoning about knowledge (epistemic logics) or about obligations and prohibitions (deontic logics), hypothetical and plausible reasoning (conditional logics), and reasoning on separation and sharing of resources (bunched implications logics). Apart from formalizing reasoning, the logics are used also to model systems and to prove properties about them, leading for example to applications in software verification.

The workshop will focus on the proof theory for such non-classical logics with the study of various calculi (proof systems). The main concern is the study of analytic calculi, with rules that compose (decompose, in the case of a tableaux calculus) the formulas to be proved in a stepwisemanner. Proofs from an analytic calculus possess the subformula property, that allows us to restrict the form of the proofs and can be exploited to prove important meta-logical properties of the formalized logics (e.g. consistency, decidability, interpolation) and to develop automated reasoning methods. In general, analytic calculi can be classified into two categories: internal calculi (for instance with sequents, hypersequents, nested sequents and tree-sequents), in which every basic object of the calculus can be read as a formula in the language of the logic; external calculi (for instance display calculi, labelled tableaux, labelled sequent calculi, bi-coloured and resource graphs) in which every basic object of the calculus cannot be read as a formula in the language of the logic. In such cases the basic objects are typically formulas of a more expressive language which imports or partially encodes the logic's semantics.

The purpose of this workshop would be to discuss recent results on analytic (external or internal) calculi for non-classical logics like intuitionistic, modal, epistemic logics, conditional logics, substructural, resouce logics, and other logical systems. Among some key points we can mention the relationships between \emph{internal} and \emph{external} calculi for such logics and also their use for studying proof-search, automated deduction (proof-theory and implementation) and also logical properties like decidability, conservativity, axiomatisations and interpolation.

The workshop is intended to provide a forum for discussion between researchers interested in topics including, but not limited to, the following areas:

• External and internal calculi for non-classical logics
• Relationships and embeddings (translations) between calculi, interactions between syntax and semantics
• New calculi for studying problems like decidability, conservativity and interpolation
• Proof-search and countermodel generation
• Methodologies and tools for translations between calculi
• Implementations of analytic calculi, proof assistants

Then we envisage a range of perspectives: proof-theoretic foundations, including decidability and complexity; model-theoretic, including semantic foundations (e.g., new semantics), modelling and verification of programs and systems.

Submissions

Researchers interested in presenting their works are invited to submit an extended abstract (up to 10 pages) through Easychair: https://easychair.org/conferences/?conf=eicncl2018r.

Papers will be reviewed by peers, typically members of the program committee.

Important Dates

Keynote speakers

Anupam Das - University of Copenhagen: Cyclic proofs, hypersequents and Kleene algebra

Dirk Pattinson - Australian National University: Infinite Formulae and Fragments of the Modal mu-Calculus

Accepted papers

- T. Dalmonte, Ch. Grellois and N. Olivetti. Toward intuitionistic non-normal modal logic and its calculi..

- C. Fiorentini and M. Ferrari. A Forward Calculus for Countermodel Construction in IPL.

- D. Galmiche, D. Mery and M. Marti. Proof Translations in BI logic.

- M. Girlando, B. Lellmann and N. Olivetti. Hypersequent calculus for the logic of conditional belief: preliminary results.

- T. Kawano. Sequent Calculi for Logic that Includes an Infinite Number of Modalities.

- T. Lyon. Effective Translations between Display and Labelled Proofs for Tense Logics.

- E. Orlandelli and S. Negri. Proof theory for quantified monotone modal logics.

- B. Więckowski. Intuitionistic multi-agent subatomic natural deduction for belief and knowledge.

Programme

The preliminary programme is now available.

Program Committee