Proceedings

Available online:

http://link.springer.com/openurl.asp?genre=issue&issn=0302-9743&volume=14278

Program

All Tableaux talks are in the Red Room.

Tuesday 19th September
08:40-09:00	Registration/Front desk
09:00-09:05	Conference welcome
09:05-09:25	Wolfgang Bibel Invited Talk	Reasoning Research Viewed in Broad Terms
09:25-10:25	Roman Kuznets Invited Talk	Always Look on Both Sides of Proof (Chair: Jens Otten)
10:25-10:50	Ian Shillito, Iris van der Giessen, Rajeev Gore and Rosalie Iemhoff	A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
10:50-11:20	Coffee break (Respirium)
	Session: Sequent calculi (Chair: TBA)
11:20-11:45	Timo Lang	Some Analytic Systems of Rules
11:45-12:10	Andrzej Indrzejczak and Nils Kürbis	A cut-free, sound and complete Russellian theory of definite descriptions
12:10-12:35	Andrzej Indrzejczak	Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators
12:35-14:00	Lunch (Respirium)
	Session: Modal logics I (Chair: Andrzej Indrzejczak)
14:00-15:00	Rosalie Iemhoff Invited Talk	Proof Systems and Termination
15:00-15:25	Iris van der Giessen, Raheleh Jalali and Roman Kuznets	Extensions of K5: Proof Theory and Uniform Lyndon Interpolation
15:25-15:50	Anupam Das and Sonia Marin	On intuitionistic diamonds (and lack thereof)
15:50-16:20	Coffee break (Respirium)
	Session: Modal logics II (Chair: Roman Kuznets)
16:20-16:45	Tiziano Dalmonte and Andrea Mazzullo	NP Complexity for Combinations of Non-Normal Modal Logics
16:45-17:10	Dirk Pattinson, Nicola Olivetti and Cláudia Nalon	Resolution-based Calculi for Non-Normal Modal Logics
17:10-17:35	Tim Lyon and Eugenio Orlandelli	Nested Sequents for Quantified Modal Logics
17:35-18:00	Matteo Acclavio, Davide Catta and Federico Olimpieri	Canonicity of Proofs in Constructive Modal Logic
Wednesday 20th September
08:40-09:00	Registration/Front desk
09:00-10:00	Valentin Goranko Invited Talk - Joint with FroCoS	Combining Semantic Tableaux (Chair: Rosalie Iemhoff)
10:00-10:30	Coffee break (Respirium)
	Session: Tableaux calculi (Chair: Nicolas Peltier)
10:30-10:55	Christoph Wernhard	Range-Restricted and Horn Interpolation through Clausal Tableaux
10:55-11:10	Carlos Areces, Valentin Cassano, Raul Fervari and Guillaume Hoffmann	DefTab: A Tableaux System for Sceptical Consequence in Default Modal Logics (Short Paper)
11:10-11:35	Ineke Van Der Berg, Andrea De Domenico, Giuseppe Greco, Krishna Manoorkar, Alessandra Palmigiano and Mattia Panettiere	Non-distributive description logic
	Session: Separation Logics (Chair: Didier Galmiche)
11:35-12:00	Frank de Boer, Hans Dieter Hiep and Stijn de Gouw	The Logic of Separation Logic: Models and Proofs
12:00-12:25	Nicolas Peltier	Testing the Satisfiability of Formulas in Separation Logic with Permissions
12:25-14:00	Lunch (Respirium)
	Excursion & Conference dinner
14:00-18:00	Transport and excursion to Karlštejn castle
18:00-22:00	Transport and conference dinner in Unětice
Thursday 21th September
	Session: Linear logic and MV-algebras I (Chair: Revantha Ramanayake)
09:00-09:25	Alexander Gheorghiu, Tao Gu and David Pym	Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic
09:25-10:25	Marta Bílková Invited Talk - Joint with FroCoS	Epistemic Logics of Structured Intensional Groups: Agents - groups - names-types
10:25-10:55	Coffee break (Respirium)
	Session: Linear Logic and MV-algebras II (Chair: Timo Lang)
10:55-11:20	Zuzana Haniková, Felip Manyà and Amanda Vidal	The MaxSAT problem in the real-valued MV-algebra
	Session: Non-wellfounded proofs (Chair: Sonia Marin)
11:20-11:45	Alexis Saurin	A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points
11:45-12:10	Bahareh Afshari, Lide Grotenhuis, Graham Leigh and Lukas Zenger	Ill-founded Proof Systems For Intuitionistic Linear-time Temporal Logic
12:10-12:35	Maurice Dekker, Johannes Kloibhofer, Johannes Marti and Yde Venema	Proof Systems for the Modal $\mu$-Calculus Obtained by Determinizing Automata
12:35-14:00	Lunch & best paper awards ceremony (Respirium)
14:00-15:00	Chad E. Brown Invited Talk - Joint with FroCoS	First-Order Instantiation-Based Tableau (Chair: Martin Suda)
15:00-15:30	Coffee break (Respirium)
	Session: Theorem proving (Chair: Josef Urban)
15:30-15:55	Michael Rawson, Christoph Wernhard, Zsolt Zombori and Wolfgang Bibel	Lemmas: Generation, Selection, Application
15:55-16:10	Bartosz Piotrowski, Ramon Fernández Mir and Edward Ayers	Machine-Learned Premise Selection for Lean (Short Paper)
16:10-16:25	Boris Shminke	gym-saturation: Gymnasium environments for saturation provers (System description) (Short Paper)
16:25-16:40	Clemens Eisenhofer, Ruba Alassaf, Michael Rawson and Laura Kovacs	Non-Classical Logics in Satisfiability Modulo Theories (Short Paper)
16:40-16:55	Asta Halkjær From and Jørgen Villadsen	A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness (Short Paper)
17:00-18:00	Business meeting