Logic, language, information, and computation : 28th International Workshop, WOLLIC 2022, Iaşi, Romania, September 20-23, 2022, proceedings / / edited by Agata Ciabattoni, Elaine Pimentel, Ruy J. G. B. de Queiroz

• Record Nr.: UNINA9910592979603321
• Pubbl/distr/stampa: Cham, Switzerland : , : Springer, , [2022]; ©2022
• ISBN: 3-031-15298-0
• Descrizione fisica: 1 online resource (441 pages)
• Collana: Lecture Notes in Computer Science ; ; v.13468
• Disciplina: 929.605
• Soggetti: Computer logic
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Nota di bibliografia: Includes bibliographical references and index.
• Nota di contenuto: Intro -- 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. &lt -- -- 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.