Logic, Language, Information, and Computation : 28th International Workshop, WoLLIC 2022, Iași, Romania, September 20–23, 2022, Proceedings

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 storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed. The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use. The publisher, the authors, and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, expressed or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. Preface Organization Invited Talks On the Proof Theoretic Strength of Circular Reasoning Open Texture and Defeasible Semantic Constraint \partial is for Dialectica How to Define Domain Specific Logics using Matching Logic The Value of Normal Derivations in the Realm of Explanations Tutorials Cardinalities, Infinities and Choice Principles for Finitely Supported Sets Intuitionistic Modal Proof Theory Automating Moral Reasoning Contents A Proof of the Focusing Theorem via MALL Proof Nets 1 Introduction 2 The MALL Fragment of Linear Logic 3 Proof Structures 4 Conclusions References Time and Gödel: Fuzzy Temporal Reasoning in PSPACE 1 Introduction 2 Syntax and Semantics 3 Real-Valued Versus Bi-relational Validity 4 Labelled Systems and Quasimodels 5 From Quasimodels to Bi-relational Models 6 From Bi-relational Models to Finite Quasimodels 7 PSPACE Completeness 8 Concluding Remarks References Fixed Point Logics and Definable Topological Properties 1 Introduction 2 Background 3 Classes Defined by Greatest Fixed Points 4 Completeness for Imperfect Spaces 5 Conclusion References Correspondence Theory for Generalized Modal Algebras 1 Introduction 2 Preliminaries 2.1 Generalized Boolean Algebras 2.2 Generalized Stone Spaces 2.3 Topological Duality Between Generalized Boolean Algebras and Generalized Stone Spaces 2.4 Adding Modality 2.5 Some Useful Propositions 3 Syntax and Semantics 3.1 Language and Syntax 3.2 Semantics 4 Preliminaries on Algorithmic Correspondence 4.1 The Expanded Language 4.2 The First-Order Correspondence Language and the Standard Translation 5 Inductive Inequalities for Generalized Modal Algebras 6 Algorithm 7 Success of ALBA 8 Soundness of ALBA 9 Right-Handed Topological Ackermann Lemma 9.1 Analysis of the Right-Handed Ackermann Rule 9.2 Proof of Topological Ackermann Lemma 10 Example 11 Concluding Remarks References Tense Logics over Lattices 1 Introduction 2 Preliminaries 2.1 Tense Logic 2.2 Step-by-Step Method 2.3 Lattices 3 TL over Lattices w.r.t. < 3.1 Arbitrary So-Lattices 3.2 Bounded So-Lattices 4 TL over Lattices w.r.t. 5 Nominal TL with "426830A sup "526930B and "426830A inf "526930B References Expressing Power of Elementary Quantum Recursion Schemes for Quantum Logarithmic-Time Computability 1 Background, Motivations, and Challenges 1.1 Schematic Definitions that Capture Quantum Computability 1.2 Our Challenges in This Work 2 Preparation: Notions and Notation 2.1 Numbers, Strings, and Languages 2.2 Quantum States and Hilbert Spaces 2.3 Conventions on the Bra and the Ket Notations 3 A Schematic Definition for EQS 3.1 Elementary Quantum Schemes 3.2 How to Deal with a Set of Different Objects 3.3 Basic Properties of EQS 4 Relationships to Quantum Computability 4.1 Comparison with Logarithmic-Time Quantum Turing Machines 4.2 Computational Complexity of BQLOGTIME References Multityped Abstract Categorial Grammars and Their Composition 1 Introduction 2 Abstract Categorial Grammars 2.1 Definitions 2.2 Distinguishing Between Structures 3 Multityped Abstract Categorial Grammars 3.1 Overloaded Signatures 3.2 Lexicons and Multityped ACGs 3.3 Multityped ACGs as Commutative Diagrams 4 The Composition Problem 4.1 Composition as Pullback 4.2 Kanazawa's Construction 5 Conclusion References Interval Probability for Sessions Types 1 Introduction 2 Processes in Probabilistic Multiparty Sessions 3 Global and Local Types 4 Interval Probability for Multiparty Session Types 5 Conclusion and Related Work References Combinatorial Flows as Bicolored Atomic Flows 1 Introduction 2 Preliminaries on Open Deduction 3 From Derivations to Flows 4 Preliminaries on RB-cographs 5 Multiplicative Flows 6 Additive Flows 7 Combinatorial Flows 8 Purification 9 Combinatorial Flows and Combinatorial Proofs 10 Conclusion and Future Work References A Logic of ``Black Box'' Classifier Systems 1 Introduction 2 Language and Semantics 3 Axiomatics and Complexity 3.1 Alternative Kripke Semantics 3.2 Finite-Variable Case 3.3 Infinite-Variable Case 3.4 Complexity Results 4 Application 4.1 An Example of Classification Task 4.2 Explanations 5 Dynamic Extension 6 Conclusion References What Kinds of Connectives Cause the Difference Between Intuitionistic Predicate Logic and the Logic of Constant Domains? 1 Introduction 1.1 Background—Generalized Kripke Semantics 1.2 Predicate Logic with General Propositional Connectives 2 Preliminaries 2.1 Truth Functions 2.2 Formulas and Sequents 2.3 Kripke Semantics 3 Condition for FOILS(C) = FOCLS(C) 3.1 The ``if'' Part 3.2 The ``only if'' Part 4 Conclusion References Logic of Visibility in Social Networks 1 Introduction 2 Related Work: Visibility and Reachability 3 Reasoning About Visibility in a Static Setting 3.1 Language and Semantics of SVL 3.2 Soundness, Completeness and Model Checking of SVL 3.3 Expressing Visibility 4 Visibility Logic 4.1 Example: Taking the Advantage to Be Seen by Many 4.2 Language, Semantics, and Logical Properties of VL 4.3 Expressivity and Model Checking 5 Conclusion and Future Work References The Alternation Hierarchy of the -calculus over Weakly Transitive Frames 1 Introduction 2 Preliminaries 3 The Collapse to the Alternation-Free Fragment over Weakly Transitive Frames 4 The Collapse over Topological Semantics 5 The Collapse over S4.2, S4.3, S4.3.2, S4.4 and KD45 6 Epistemic Logic and Ignorance References Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Tests 1 Introduction 2 KAT and S 2.1 Kleene Algebra with Tests 2.2 Substructural Logic of Partial Correctness 3 Residuated KAT 4 Kleene Algebra with Codomain 5 SKAT: Residuated KAC with a Galois Connection 6 The Embedding Result 7 Conclusion References The Limits to Gossip: Second-Order Shared Knowledge of All Secrets is Unsatisfiable 1 Introduction 2 Related Work 3 Syntax and Semantics 4 Causal Relation and Causal Cone 5 Lucky Calls 6 Main Result 7 Conclusion and Open Questions References Additive Types in Quantitative Type Theory 1 Introduction 1.1 Contributions 1.2 Structure 2 Related Work 3 Quantitative Type Theory 3.1 Semirings 3.2 Typing Rules 3.3 Weakening 4 Multiplicative Types 4.1 Multiplicative Pairs 4.2 Multiplicative Unit 4.3 Exponential Modality 4.4 Extended Eliminator 5 Additive Types 5.1 Additive Unions 5.2 Additive Zero 5.3 Additive Pairs 5.4 Additive Unit 5.5 Usage 6 Bidirectional Type System 7 Implementation 7.1 Language Interpreter 7.2 Typing Algorithm 8 Conclusion References Strongly First Order, Domain Independent Dependencies: The Union-Closed Case 1 Introduction 2 Preliminaries 3 Characterizing Union-Closed Dependencies 4 Conclusion References Towards an Intuitionistic Deontic Logic Tolerating Conflicting Obligations 1 Introduction 2 The Logics MIND and MIND+ 3 Sequent Calculi 4 Conclusions References Presburger Büchi Tree Automata with Applications to Logics with Expressive Counting 1 Introduction 2 Preliminaries 3 Suitable Tree Automata Models 4 Non-emptiness Problem for PBTA is in NP 5 Non-emptiness for SPBTA 6 Applications in Logic References Abstract Cyclic Proofs 1 Introduction 2 Cyclic Proofs for the Modal -Calculus 3 Abstracting the Trace Condition 4 Abstract Cyclic Derivations 5 A Ramsey-Based Soundness Condition 6 PSPACE-Completeness of Cyclic Proof Checking 7 Conclusion 7.1 Related Work 7.2 Future Work References Subordination Algebras as Semantic Environment of Input/Output Logic 1 Introduction 2 Preliminaries 3 Proto-Subordination Algebras and Slanted Algebras 4 Applications 5 Conclusions and Related Works References Material Dialogues for First-Order Logic in Constructive Type Theory 1 Introduction 1.1 Outline and Contributions 2 Preliminaries 2.1 The Calculus of Inductive Constructions 2.2 First-Order Predicate Logic 2.3 De Bruijn Binders 3 Classical Material Dialogues 4 Intuitionistic Material Dialogues 5 Discussion References On the Computational Properties of the Uncountability of the Real Numbers 1 Introduction 1.1 Motivation and Overview 1.2 Volterra's Early Work and Related Results 1.3 Preliminaries and Definitions 2 Main Results 2.1 Introduction 2.2 Computational Equivalences for Strong Cantor Realisers 3 Some Details of Kleene's Computability Theory References Mining the Surface: Witnessing the Low Complexity Theorems of Arithmetic 1 Introduction 2 Preliminaries 3 A Polynomial-time Notation System for 0 4 The System TI(1, ) 4.1 A Proof System for TI(1, ) 5 Witnessing Flows References Non-monotonic Reasoning via Dynamic Consequence 1 Introduction 2 Preliminaries 3 From Classical to Default Consequence 4 From Pivotal Rules to Model Updates 4.1 Pivotal Consequence in PAL 4.2 Credulous Consequence in PAL 5 Final Remarks References Author Index Edited in collaboration with FoLLI, the Association of Logic, Language and Information this book constitutes the refereed proceedings of the 28th Workshop on Logic, Language, Information and Computation, WoLLIC 2022, Iasi, Romania, in September 2022. The 25 full papers presented included with 8 extra abstracts, 5 invited talks and 3 tutorials were fully reviewed and selected from 46 submissions. The conference aims fostering interdisciplinary research in pure and applied logic.