Logic, Language, Information, and Computation : 25th International Workshop, WoLLIC 2018, Bogota, Colombia, July 24-27, 2018, Proceedings

Edited in collaboration with FoLLI, the Association of Logic, Language and Information this book constitutes the refereed proceedings of the 25th Workshop on Logic, Language, Information and Communication, WoLLIC 2018, held inBogota, Colombia, in July 2018. The 16 full papers together with 3 short papers and 3 invited talks presented were fully reviewed and selected from 30 submissions. The vision for the conference is to provide an annual forum which is large enough to provide meaningful interactions between logic and the sciences related to information and computation. Preface 6 Organization 7 Abstracts of Invited Talks 8 Inhabitants of Intuitionistic Implicational Theorems 9 Generic Models on Sheaves 9 Symbolic Reasoning Methods in Rewriting Logic and Maude 11 A Semantical View of Proof Systems 12 Dynamics of Knowledge: Belief Revision and Argumentation 13 Revising System Specifications in Temporal Logic 11 Contents 16 Inhabitants of Intuitionistic Implicational Theorems 18 1 Introduction 18 2 Some Other Approaches 19 3 A New Sequent Calculus for J 19 4 Standard Proofs, Cafs and an Inhabitant 26 4.1 Tracing Occurrences 31 4.2 Formulas Turned into Caf's 34 4.3 BB'I-Abstraction 36 4.4 Correctness 38 5 Conclusions 39 References 40 Symbolic Reasoning Methods in Rewriting Logic and Maude 42 1 Introduction 42 1.1 Rewriting Logic as a Logical and Semantic Framework 43 1.2 Maude 43 1.3 Symbolic Reasoning Methods 44 1.4 Symbolic Methods for Rewriting Logic in a Nutshell 45 1.5 Ecumenical Scope 47 2 Symbolic Methods for Rewriting Logic 48 2.1 Tree Automata and Term Pattern Methods 48 2.2 Equational Unification and Generalization 52 2.3 Methods for Satisfiability Modulo a Theory 56 2.4 Symbolic Reachability Analysis 58 2.5 Symbolic LTL Model Checking of Infinite-State Systems 61 2.6 Constructor-Based Reachability Logic 63 3 Maude-Based Symbolic Reasoning Engines 64 3.1 Symbolic Reasoning Engines 64 3.2 Prototypes 66 4 Some Application Areas 68 5 Conclusions 68 References 69 A Semantical View of Proof Systems 78 1 Introduction 78 2 Sequent Systems 79 3 Nested Systems 80 3.1 Sequentialising Nested Systems 81 4 Labelled Proof Systems 83 5 Intuitionistic Logic 85 6 Normal Modal Logics 86 7 Non-normal Modal Systems 88 8 Conclusion and Future Work 91 References 92 A Formalization of Brouwer's Argument for Bar Induction 94 1 Introduction 94 2 Definitions of Formal Systems 97 3 Embedding of Brouwer's Bar Induction 101 4 Normalization Theorem 104 5 Conclusion and Remarks 105 References 106 Deciding Open Definability via Subisomorphisms 108 1 Introduction 108 2 Preliminaries 109 3 Computing OpenDef Efficiently 111 4 Implementation 112 5 Empirical Tests 114 5.1 On the Number of Isomorphism Types of Submodels 115 5.2 Tests with Definable Target 115 5.3 Tests with Non-definable Target 117 6 Conclusions and Future Work 118 References 121 APAL with Memory Is Better 123 1 Introduction 123 2 Syntax, Semantics, and Axiomatization 126 3 An Analysis of Kuijer's Counterexample 130 4 Soundness, via Pseudo-model Semantics 132 5 Completeness 139 6 Expressivity 143 7 Conclusions and Future Work 144 References 144 Lindenbaum and Pair Extension Lemma in Infinitary Logics 147 1 Introduction 147 2 Preliminaries 149 3 Lindenbaum Lemma for Some Infinitary Logics 152 4 Pair Extension Lemma 156 5 Conclusion and Future Work 160 References 160 The Epistemology of Nondeterminism 162 1 Introduction 162 2 Review and Motivation 163 3 Topology, Dynamics, and Determinism 165 3.1 Topological Spaces and Models 165 3.2 Dynamic Topological Models 166 3.3 Determinism as Continuity 167 4 Axiomatization and Model Transformation 168 5 Knowledge and Learning 171 5.1 Incorporating Knowledge 171 5.2 Test Programs and Public Announcements 173 6 Future Work 174 A Proofs and Details 174 A.1 Characterizing Continuity 174 A.2 Model Transformation 175 A.3 Sequencing 176 A.4 Dynamic Topological Epistemic Logic 177 References 179 Parameterized Complexity of Some Prefix-Vocabulary Fragments of First-Order Logic 180 1 Introduction 180 2 Preliminaries 182 2.1 Decidable Prefix-Vocabulary Fragments 182 2.2 Parameterized Complexity 185 3 The Parameterized Complexity of Classical Decidable Classes 186 3.1 The Löwenheim Class and the Löwenheim Class with Equality 187 3.2 The Bernays-Schönfinkel-Ramsey Class 188 3.3 The Ackermann and Gödel-Kalmár-Shütte Classes 188 4 Modest Complexity Prefix-Vocabulary Classes 189 5 Conclusion 190 References 194 Unification Modulo Builtins 196 1 Introduction 196 2 Constrained Terms 199 3 E-Unification Modulo Builtins 203 4 An Algorithm for E-Unification Modulo Builtins 204 5 Conclusion and Future Work 207 A Maude Prototype 208 References 211 Formalization of the Undecidability of the Halting Problem for a Functional Language 213 1 Introduction 213 2 Semantic Termination 214 3 Partial Recursive Functions 219 4 Undecidability of the Halting Problem 221 5 Related Work 223 6 Conclusion and Future Work 224 References 225 Handling Verb Phrase Anaphora with Dependent Types and Events 227 1 Introduction 227 2 Recalling Dependent Type Semantics 228 3 Verb Phrase Anaphora 231 4 Events with Dependent Types 232 5 Subtyping 236 6 Comparison with Previous Approaches 237 7 Conclusion 238 References 238 Parameterized Complexity for Uniform Operators on Multidimensional Analytic Functions and ODE Solving 240 1 Introduction 240 2 Computability and Complexity in Analysis 242 2.1 Complexity Theory 243 3 Uniform Computations on Analytic Functions 244 3.1 Representing Power Series 245 3.2 Representing Analytic Functions 247 4 Ordinary Differential Equations 249 5 Practical Considerations 250 6 Conclusion 251 References 252 Advanced Kripke Frame for Quantum Logic 254 1 Introduction 254 2 Basics 255 3 DOM-Frame 257 4 Related Sequent Calculus and Future Work 262 References 266 The Undecidability of Orthogonal and Origami Geometries 267 1 Introduction and Summary of Results 267 2 Plane Geometry 272 3 Background on Fields 274 4 From Fields to Planes 275 5 From Planes to Fields 276 6 Undecidable Geometries 277 6.1 Incidence Geometries 277 6.2 Hilbert Planes and Euclidean Planes 278 6.3 Wu's Geometry 278 6.4 Origami Geometry 279 A Axioms for Affine Geometries 279 A.1 Incidence Geometries 279 A.2 Hilbert Style Geometries 280 A.3 Axioms of Orthogonal Geometry 282 A.4 The Origami Axioms 282 B Translation Schemes 284 References 285 Algebraic Semantics for Nelson's Logic S 288 1 Introduction 288 2 Nelson's Logic S 290 3 S Is Algebraizable 293 3.1 S-algebras 294 3.2 Alternative Presentation of S-algebras 295 4 A Finite Hilbert-Style Calculus for S 296 5 Comparing S with N3 and N4 298 5.1 N4 298 5.2 N3 300 6 Future Work 300 References 304 Beliefs Based on Evidence and Argumentation 306 1 Introduction 306 2 Preliminaries 308 3 Belief, Evidence, Argumentation, and Their Logic 310 3.1 The Logic of Belief, Evidence and Argumentation 312 4 Further Epistemic Notions 315 5 Conclusion and Future Work 317 A Completeness for LAbat 318 References 322 The Effort of Reasoning: Modelling the Inference Steps of Boundedly Rational Agents 324 1 Introduction 324 2 The Logical Framework to Model the Effort of Inference Steps 326 2.1 Syntax 326 2.2 Plausibility Models 327 2.3 Model Transformations and Semantic Clauses 329 2.4 Discussion 331 3 Reduction and Axiomatization 332 3.1 The (Static) Language for the Reduction 333 3.2 Building the Reduced Model 333 3.3 Axiomatization 334 4 Conclusions and Further Research 335 References 340 Author Index 342 Front Matter ....Pages I-XVIII Inhabitants of Intuitionistic Implicational Theorems (Katalin Bimbó)....Pages 1-24 Symbolic Reasoning Methods in Rewriting Logic and Maude (José Meseguer)....Pages 25-60 A Semantical View of Proof Systems (Elaine Pimentel)....Pages 61-76 A Formalization of Brouwer’s Argument for Bar Induction (Ryota Akiyoshi)....Pages 77-90 Deciding Open Definability via Subisomorphisms (Carlos Areces, Miguel Campercholi, Pablo Ventura)....Pages 91-105 APAL with Memory Is Better (Alexandru Baltag, Aybüke Özgün, Ana Lucia Vargas Sandoval)....Pages 106-129 Lindenbaum and Pair Extension Lemma in Infinitary Logics (Marta Bílková, Petr Cintula, Tomáš Lávička)....Pages 130-144 The Epistemology of Nondeterminism (Adam Bjorndahl)....Pages 145-162 Parameterized Complexity of Some Prefix-Vocabulary Fragments of First-Order Logic (Luis Henrique Bustamante, Ana Teresa Martins, Francicleber Ferreira Martins)....Pages 163-178 Unification Modulo Builtins (Ştefan Ciobâcă, Andrei Arusoaie, Dorel Lucanu)....Pages 179-195 Formalization of the Undecidability of the Halting Problem for a Functional Language (Thiago Mendonça Ferreira Ramos, César Muñoz, Mauricio Ayala-Rincón, Mariano Moscato, Aaron Dutle, Anthony Narkawicz)....Pages 196-209 Handling Verb Phrase Anaphora with Dependent Types and Events (Daniyar Itegulov, Ekaterina Lebedeva)....Pages 210-222 Parameterized Complexity for Uniform Operators on Multidimensional Analytic Functions and ODE Solving (Akitoshi Kawamura, Florian Steinberg, Holger Thies)....Pages 223-236 Advanced Kripke Frame for Quantum Logic (Tomoaki Kawano)....Pages 237-249 The Undecidability of Orthogonal and Origami Geometries (J. A. Makowsky)....Pages 250-270 Algebraic Semantics for Nelson’s Logic \(\mathcal {S}\) (Thiago Nascimento, Umberto Rivieccio, João Marcos, Matthew Spinks)....Pages 271-288 Beliefs Based on Evidence and Argumentation (Chenwei Shi, Sonja Smets, Fernando R. Velázquez-Quesada)....Pages 289-306 The Effort of Reasoning: Modelling the Inference Steps of Boundedly Rational Agents (Sonja Smets, Anthia Solaki)....Pages 307-324 Back Matter ....Pages 325-325