WEIC 2018 - International Workshop on EXTERNAL AND INTERNAL CALCULI FOR NON-CLASSICAL LOGICS

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