Automated Reasoning with Analytic Tableaux and Related Methods: 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings (Lecture Notes in Computer Science, 11714)

This book constitutes the proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019, held in London, UK, in September 2019, colocated with the 12th International Symposium on Frontiers on Combining Systems, FroCoS 2019. The 25 full papers presented were carefully reviewed and selected from 43 submissions.They present research on all aspects of the mechanization of tableaux-based reasoning and related methods, including theoretical foundations, implementation techniques, systems development and applications. The papers are organized in the following topical sections: tableau calculi, sequent calculi, semantics and combinatorial proofs, non-wellfounded proof systems, automated theorem provers, and logics for program or system verification. Front Matter ....Pages i-xxi Front Matter ....Pages 1-1 A SAT-Based Encoding of the One-Pass and Tree-Shaped Tableau System for LTL (Luca Geatti, Nicola Gigante, Angelo Montanari)....Pages 3-20 Certification of Nonclausal Connection Tableaux Proofs (Michael Färber, Cezary Kaliszyk)....Pages 21-38 Preferential Tableaux for Contextual Defeasible \(\mathcal {ALC}\) (Katarina Britz, Ivan Varzinczak)....Pages 39-57 A Tableau Calculus for Non-clausal Maximum Satisfiability (Chu Min Li, Felip Manyà, Joan Ramon Soler)....Pages 58-73 Front Matter ....Pages 75-75 First-Order Quasi-canonical Proof Systems (Yotam Dvir, Arnon Avron)....Pages 77-93 Bounded Sequent Calculi for Non-classical Logics via Hypersequents (Agata Ciabattoni, Timo Lang, Revantha Ramanayake)....Pages 94-110 A Proof-Theoretic Perspective on SMT-Solving for Intuitionistic Propositional Logic (Camillo Fiorentini, Rajeev Goré, Stéphane Graham-Lengrand)....Pages 111-129 Relating Labelled and Label-Free Bunched Calculi in BI Logic (Didier Galmiche, Michel Marti, Daniel Méry)....Pages 130-146 Sequentialising Nested Systems (Elaine Pimentel, Revantha Ramanayake, Björn Lellmann)....Pages 147-165 A Hypersequent Calculus with Clusters for Data Logic over Ordinals (Anthony Lick)....Pages 166-184 Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents (Rajeev Goré, Björn Lellmann)....Pages 185-202 Combining Monotone and Normal Modal Logic in Nested Sequents – with Countermodels (Björn Lellmann)....Pages 203-220 Front Matter ....Pages 221-221 On Combinatorial Proofs for Modal Logic (Matteo Acclavio, Lutz Straßburger)....Pages 223-240 A Game Model for Proofs with Costs (Timo Lang, Carlos Olarte, Elaine Pimentel, Christian G. Fermüller)....Pages 241-258 Towards a Combinatorial Proof Theory (Benjamin Ralph, Lutz Straßburger)....Pages 259-276 Birkhoff Completeness for Hybrid-Dynamic First-Order Logic (Daniel Găină, Ionuţ Ţuţu)....Pages 277-293 Front Matter ....Pages 295-295 Infinets: The Parallel Syntax for Non-wellfounded Proof-Theory (Abhishek De, Alexis Saurin)....Pages 297-316 PSPACE-Completeness of a Thread Criterion for Circular Proofs in Linear Logic with Least and Greatest Fixed Points (Rémi Nollet, Alexis Saurin, Christine Tasson)....Pages 317-334 A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic (Simon Docherty, Reuben N. S. Rowe)....Pages 335-352 Front Matter ....Pages 353-353 Herbrand Constructivization for Automated Intuitionistic Theorem Proving (Gabriel Ebner)....Pages 355-373 ENIGMAWatch: ProofWatch Meets ENIGMA (Zarathustra Goertzel, Jan Jakubův, Josef Urban)....Pages 374-388 Front Matter ....Pages 389-389 Behavioral Program Logic (Eduard Kamburjan)....Pages 391-408 Prenex Separation Logic with One Selector Field (Mnacho Echenim, Radu Iosif, Nicolas Peltier)....Pages 409-427 Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems (João G. Martins, André Platzer, João Leite)....Pages 428-445 Operational Semantics and Program Verification Using Many-Sorted Hybrid Modal Logic (Ioana Leuştean, Natalia Moangă, Traian Florin Şerbănuţă)....Pages 446-476 Back Matter ....Pages 477-477 This book constitutes the proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019, held in London, UK, in September 2019, colocated with the 12th International Symposium on Frontiers on Combining Systems, FroCoS 2019. The 25 full papers presented were carefully reviewed and selected from 43 submissions. They present research on all aspects of the mechanization of tableaux-based reasoning and related methods, including theoretical foundations, implementation techniques, systems development and applications. The papers are organized in the following topical sections: tableau calculi, sequent calculi, semantics and combinatorial proofs, non-wellfounded proof systems, automated theorem provers, and logics for program or system verification