EXTERNAL AND INTERNAL CALCULI FOR NON-CLASSICAL LOGICS
(associated with FLOC 2018 and with IJCAR 2018)
Oxford, England, UK.
July 19, 2018.
A special issue of a Journal is expected on these topics, with a deadline for submission of approximately 3 ou 4 months 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:
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 ``WEIC 2018 submission'') of a PDF file to to Didier Galmiche (Didier.Galmiche@loria.fr) by April 20th 2018 .
Papers will be reviewed by peers, typically members of the programme committee.
The workshop is co-organized by A. Ciabattoni, R. Ramanayake (TU Vienna), N. Olivetti (LSIS, Aix-marseille University) and D. Galmiche (LORIA - Lorraine University).
It will be supported by Austrian-French (ANR-FWF) project TICAMORE