EXTERNAL AND INTERNAL CALCULI FOR NON-CLASSICAL LOGICS

(affiliated with IJCAR 2018)

* Oxford, England, UK.
*

* July 18, 2018. *

A one day workshop on

A special issue of a Journal is expected on these topics after the workshop.

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
- Protype 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.

TBA

Researchers interested in presenting their works are invited to send an
** extended abstract (up to 10 pages)} by e-mail submission (with the
subject line ``CNCL2018 submission'') of a PDF file ** to ....
by ** ..... 2018 **.
Papers will be reviewed by peers, typically members of the programme
committee.

TBA

TBA