Sergei Artemov Anil Nerode (Eds.) 3 0 7 Logical Foundations 0 1 S C of Computer Science N L International Symposium, LFCS 2018 Deerfield Beach, FL, USA, January 8–11, 2018 Proceedings 123 Lecture Notes in Computer Science 10703 Commenced Publication in 1973 Founding and Former Series Editors: Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen Editorial Board David Hutchison Lancaster University, Lancaster, UK Takeo Kanade Carnegie Mellon University, Pittsburgh, PA, USA Josef Kittler University of Surrey, Guildford, UK Jon M. Kleinberg Cornell University, Ithaca, NY, USA Friedemann Mattern ETH Zurich, Zurich, Switzerland John C. Mitchell Stanford University, Stanford, CA, USA Moni Naor Weizmann Institute of Science, Rehovot, Israel C. Pandu Rangan Indian Institute of Technology, Madras, India Bernhard Steffen TU Dortmund University, Dortmund, Germany Demetri Terzopoulos University of California, Los Angeles, CA, USA Doug Tygar University of California, Berkeley, CA, USA Gerhard Weikum Max Planck Institute for Informatics, Saarbrücken, Germany More information about this series at http://www.springer.com/series/7407 Sergei Artemov Anil Nerode (Eds.) (cid:129) Logical Foundations of Computer Science International Symposium, LFCS 2018 fi – Deer eld Beach, FL, USA, January 8 11, 2018 Proceedings 123 Editors SergeiArtemov Anil Nerode City University of NewYork Cornell University NewYork,NY Ithaca, NY USA USA ISSN 0302-9743 ISSN 1611-3349 (electronic) Lecture Notesin Computer Science ISBN 978-3-319-72055-5 ISBN978-3-319-72056-2 (eBook) https://doi.org/10.1007/978-3-319-72056-2 LibraryofCongressControlNumber:2017960856 LNCSSublibrary:SL1–TheoreticalComputerScienceandGeneralIssues ©SpringerInternationalPublishingAG2018 Thisworkissubjecttocopyright.AllrightsarereservedbythePublisher,whetherthewholeorpartofthe material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or information storageandretrieval,electronicadaptation,computersoftware,orbysimilarordissimilarmethodologynow knownorhereafterdeveloped. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Thepublisher,theauthorsandtheeditorsaresafetoassumethattheadviceandinformationinthisbookare believedtobetrueandaccurateatthedateofpublication.Neitherthepublishernortheauthorsortheeditors give a warranty, express or implied, with respect to the material contained herein or for any errors or omissionsthatmayhavebeenmade.Thepublisherremainsneutralwithregardtojurisdictionalclaimsin publishedmapsandinstitutionalaffiliations. Printedonacid-freepaper ThisSpringerimprintispublishedbySpringerNature TheregisteredcompanyisSpringerInternationalPublishingAG Theregisteredcompanyaddressis:Gewerbestrasse11,6330Cham,Switzerland Preface TheSymposiumonLogicalFoundationsofComputerScienceprovidesaforumforthe fast-growing body of work on the logical foundations of computer science, e.g., those areas of fundamental theoretical logic related to computer science. The LFCS series began with “Logic at Botik,” Pereslavl-Zalessky, 1989, which was co-organized by Albert R.Meyer (MIT) and Michael Taitslin(Tver).Afterthat,organizationpassed to Anil Nerode. Currently LFCS is governed by a Steering Committee consisting of Anil Nerode (General Chair), Stephen Cook, Dirk van Dalen, Yuri Matiyasevich, Gerald Sacks, Andre Scedrov, and Dana Scott. The 2018 Symposium on Logical Foundations of Computer Science (LFCS 2018) took place at the Wyndham Deerfield Beach Resort, Deerfield Beach, Florida, USA, during January 8–11, 2018. This volume contains the extended abstracts of talks selected by the Program Committee for presentation at LFCS 2018. The scope of the symposium is broad and includes constructive mathematics and type theory, homotopy type theory, logic, automata and automatic structures, com- putability and randomness, logical foundations of programming, logical aspects of computational complexity, parameterized complexity, logic programming and con- straints, automated deduction and interactive theorem proving, logical methods in protocol and program verification, logical methods in program specification and extraction, domain theory logics, logical foundations of database theory, equational logic and term rewriting, lambda and combinatory calculi, categorical logic and topological semantics, linear logic, epistemic and temporal logics, intelligent and multiple-agent system logics, logics of proof and justification, non-monotonic rea- soning, logic in game theory and social software, logic of hybrid systems, distributed system logics, mathematical fuzzy logic, system design logics, and other logics in computer science. We thank the authors and reviewers for their contributions. We acknowledge the supportoftheU.S.NationalScienceFoundation,TheAssociationforSymbolicLogic, Cornell University, the Graduate Center of the City University of New York, and Florida Atlantic University. October 2017 Anil Nerode Sergei Artemov Organization Steering Committee Stephen Cook University of Toronto, Canada Yuri Matiyasevich Steklov Mathematical Institute, St. Petersburg, Russia AnilNerode(GeneralChair) Cornell University, USA Gerald Sacks Harvard University, USA Andre Scedrov University of Pennsylvania, USA Dana Scott Carnegie-Mellon University, USA Dirk van Dalen Utrecht University, The Netherlands Program Committee Sergei Artemov (Chair) The City University of New York, USA Eugene Asarin Université Paris Diderot - Paris 7, France Steve Awodey Carnegie Mellon University, USA Matthias Baaz The Vienna University of Technology, Austria Lev Beklemishev Steklov Mathematical Institute, Moscow, Russia Andreas Blass University of Michigan, Ann Arbor, USA Samuel Buss University of California, San Diego, USA Robert Constable Cornell University, USA Thierry Coquand University of Gothenburg, Sweden Nachum Dershowitz Tel Aviv University, Israel Michael Fellows University of Bergen, Norway Melvin Fitting The City University of New York, USA Sergey Goncharov Sobolev Institute of Mathematics, Novosibirsk, Russia Denis Hirschfeldt University of Chicago, USA Martin Hyland University of Cambridge, UK Rosalie Iemhoff Utrecht University, The Netherlands Hajime Ishihara Japan Advanced Institute of Science and Technology, Kanazawa, Japan Bakhadyr Khoussainov The University of Auckland, New Zealand Roman Kuznets The Vienna University of Technology, Austria Daniel Leivant Indiana University Bloomington, USA Robert Lubarsky Florida Atlantic University, USA Victor Marek University of Kentucky, Lexington, USA Lawrence Moss Indiana University Bloomington, USA Anil Nerode Cornell University, USA Hiroakira Ono Japan Advanced Institute of Science and Technology, Kanazawa, Japan Alessandra Palmigiano Delft University of Technology, The Netherlands Ruy de Queiroz The Federal University of Pernambuco, Recife, Brazil VIII Organization Ramaswamy Ramanujam TheInstitute ofMathematical Sciences,Chennai,India Michael Rathjen University of Leeds, UK Jeffrey Remmel University of California, San Diego, USA Andre Scedrov University of Pennsylvania, USA Helmut Schwichtenberg University of Munich, Germany Philip Scott University of Ottawa, Canada Alex Simpson University of Ljubljana, Slovenia Sonja Smets University of Amsterdam, The Netherlands Sebastiaan Terwijn Radboud University Nijmegen, The Netherlands Alasdair Urquhart University of Toronto, Canada Additional Reviewers Josef Berger S. P. Suresh Catalin Dima Giuseppe Greco Yanjing Wang Heinrich Wansing Toshiyasu Arai Lutz Straßburger Rohit Parikh Contents The Completeness Problem for Modal Logic . . . . . . . . . . . . . . . . . . . . . . . 1 Antonis Achilleos Justification Awareness Models. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Sergei Artemov A Minimal Computational Theory of a Minimal Computational Universe. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 Arnon Avron and Liron Cohen A Sequent-Calculus Based Formulation of the Extended First Epsilon Theorem. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 Matthias Baaz, Alexander Leitsch, and Anela Lolic Angluin Learning via Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 Simone Barlocco and Clemens Kupke r A Universal Algebra for the Variable-Free Fragment of RC . . . . . . . . . . . . 91 Lev D. Beklemishev A Logic of Blockchain Updates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 Kai Brünnler, Dandolo Flumini, and Thomas Studer From Display to Labelled Proofs for Tense Logics . . . . . . . . . . . . . . . . . . . 120 Agata Ciabattoni, Tim Lyon, and Revantha Ramanayake Notions of Cauchyness and Metastability. . . . . . . . . . . . . . . . . . . . . . . . . . 140 Hannes Diener and Robert Lubarsky A Gödel-Artemov-Style Analysis of Constructible Falsity . . . . . . . . . . . . . . 154 Thomas Macaulay Ferguson Probabilistic Reasoning About Simply Typed Lambda Terms. . . . . . . . . . . . 170 Silvia Ghilezan, Jelena Ivetić, Simona Kašterović, Zoran Ognjanović, and Nenad Savić Polyteam Semantics. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 190 Miika Hannula, Juha Kontinen, and Jonni Virtema On the Sharpness and the Single-Conclusion Property of Basic Justification Models. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211 Vladimir N. Krupski X Contents Founded Semantics and Constraint Semantics of Logic Rules. . . . . . . . . . . . 221 Yanhong A. Liu and Scott D. Stoller Separating the Fan Theorem and Its Weakenings II. . . . . . . . . . . . . . . . . . . 242 Robert S. Lubarsky Dialectica Categories for the Lambek Calculus. . . . . . . . . . . . . . . . . . . . . . 256 Valeria de Paiva and Harley Eades III From Epistemic Paradox to Doxastic Arithmetic. . . . . . . . . . . . . . . . . . . . . 273 V. Alexis Peluce A Natural Proof System for Herbrand’s Theorem . . . . . . . . . . . . . . . . . . . . 289 Benjamin Ralph Metastability and Higher-Order Computability . . . . . . . . . . . . . . . . . . . . . . 309 Sam Sanders The Completeness of BCD for an Operational Semantics. . . . . . . . . . . . . . . 331 Rick Statman A Tableau System for Instantial Neighborhood Logic . . . . . . . . . . . . . . . . . 337 Junhua Yu Interpretations of Presburger Arithmetic in Itself. . . . . . . . . . . . . . . . . . . . . 354 Alexander Zapryagaev and Fedor Pakhomov Author Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 369