Logic, Language, Information, and Computation : 30th International Workshop, WoLLIC 2024, Bern, Switzerland, June 10-13, 2024, Proceedings

• Record Nr.: UNINA9910865249003321
• Autore: Metcalfe George
• Pubbl/distr/stampa: Cham : , : Springer International Publishing AG, , 2024; ©2024
• ISBN: 9783031626876; 9783031626869
• Edizione: [1st ed.]
• Descrizione fisica: 1 online resource (309 pages)
• Collana: Lecture Notes in Computer Science Series ; ; v.14672
• Altri autori (Persone): StuderThomas; de QueirozRuy
• Lingua di pubblicazione: Inglese
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Nota di contenuto: Intro -- Preface -- Organization -- Invited Talks -- Model Theory of Gödel Logic -- Nøthing is Logical -- Probability and Nondeterminism with Multiset Semantics -- Theory and Practice of Uniform Interpolation -- Pride and Probability -- Contents -- Strict-Tolerant Conditional Logics -- 1 Introduction -- 2 Semantics -- 3 A Labelled Sequent Calculus for stC -- 4 Extensions -- 4.1 ID -- 4.2 MP -- 4.3 ID+MP -- 5 Connexivity -- 6 Conclusion -- References -- A Linear Proof Language for Second-Order Intuitionistic Linear Logic -- 1 Introduction -- 2 The LS2-Calculus -- 3 Correctness -- 4 Encodings -- 4.1 Vectors -- 4.2 Matrices -- 4.3 Matrix Iterator -- 5 Linearity -- 6 Conclusion -- A Proof of Section3 -- B Proof of Section5 -- References -- A Logic of Isolation -- 1 Introduction -- 2 Syntax, Proof System, and Relational Semantics -- 2.1 Axiom System -- 2.2 Relational Semantics -- 3 Neighborhood Semantics for Si -- 3.1 Semantic Insensitivities -- 3.2 Soundness and Completeness -- 4 Discrete Neighborhood Systems -- 4.1 Discrete Topologies -- 5 Conclusion and Future Work -- References -- A Simple Loopcheck for Intuitionistic K -- 1 Introduction -- 2 Preliminaries -- 3 Labelled Sequent Calculus labIKs -- 4 Models from Sequents -- 5 The Proof-Search Algorithm -- 6 Conclusions and Future Work -- A Proofs -- B Examples -- References -- A ; Compositional Theory of Krivine's Classical Realisability -- 1 Introduction -- 1.1 Conventions and Notations -- 1.2 Classical Compositional Truth -- 2 Classical Realisability -- 2.1 Classical Number Realisability -- 2.2 Compositional Theory for Realisability -- 3 Formalised Realisation of Peano Arithmetic -- 4 Proof-Theoretic Strength of Compositional Realisability -- 4.1 Compositional Realisability as Compositional Truth -- 4.2 Compositional Realisability with the Reflection Rule -- 5 Future Work.; A Well-Ordering Proof in Compositional Realisability -- References -- Intersection Types via Finite-Set Declarations -- 1 The Troublesome Intersection-Introduction Rule -- 2 Finite-Set Declarations and Encoding -Types -- 3 Extending the Syntax of the -cube -- 4 Implementing Intersection Types -- 4.1 Simple Examples -- 4.2 Typing Urzyczyn's Untypable Term -- 5 Conclusion -- References -- Syntactic Concept Lattice Models for Infinitary Action Logic -- 1 Introduction -- 2 Syntactic Concept Lattices -- 3 Completeness Proof and Corollaries -- 4 SCL-Models over a Two-Letter Alphabet -- 5 Regular SCL-Models -- References -- Rules of Partial Orthomodularity -- 1 Introduction -- 2 Preliminaries -- 3 Rules of Partial Orthomodularity -- 4 A Forbidden Subalgebra Theorem for Partial Orthomodularity -- 5 A Representation Theorem for Partial Orthomodularity -- 6 Related Work -- 7 Conclusion -- References -- Labelled Sequent Calculi for Inquisitive Modal Logics -- 1 Introduction -- 2 Inquisitive Modal Logic -- 3 Labelled Sequent Calculi for Inquisitive Modal Logics -- 4 Structural Properties -- 5 Soundness and Completeness -- 6 Conclusion -- A Proof of Theorem 1 -- B Derivations for Some of the Axioms from Figure1 -- C Derivations for the Special Axioms from Table1 -- References -- Correspondence Theory on Vector Spaces -- 1 Introduction -- 2 Preliminaries -- 2.1 Algebras over a Field and Their Complex Algebras -- 2.2 Analytic Inductive Inequalities in Residuated Lattices -- 3 Rewriting Analytic Inductive Inequalities -- 3.1 Analytic Inductive Shape in Residuated Lattices -- 3.2 Solving in the Positive Coordinates -- 3.3 From Analytic Inductive to Quasi Left Primitive -- 4 Correspondence -- 5 Conclusions -- A Examples -- References -- An EXPTIME-Complete Entailment Problem in Separation Logic -- 1 Introduction -- 2 Separation Logic with Inductive Definitions.; 3 The Entailment Problem Ent(DSH,HC) -- 4 Abstracting Structures -- 5 Computing Abstractions -- 6 Conclusion -- A Proof of Lemma 4.10 -- B Proof of Lemma 4.11 -- C Proof of Lemma 5.3 -- D Proof of Lemma 5.5 -- References -- (In)consistency Operators on Quasi-Nelson Algebras -- 1 Introduction -- 2 Quasi-Nelson Logic and Algebras -- 3 Inconsistency Operators -- 3.1 The min and B min Operators -- 3.2 The min B Operator -- 3.3 Twist Representation -- 3.4 Filters and Congruences -- 4 Future Work -- 4.1 Consistency Operators -- 4.2 LFIs Based on Quasi-Nelson Algebras -- 4.3 (In)consistency Operators Beyond the Quasi-Nelson Setting -- References -- Lambek Calculus with Banged Atoms for Parasitic Gaps -- 1 Introduction -- 2 The System -- 3 Cut Elimination -- 4 A One-Sided System -- 5 Proof Nets -- 6 Decidability and Complexity -- 7 Application to Relativisation in Natural Language -- 8 Discussion and Conclusion -- A Appendix -- References -- Completeness of Finitely Weighted Kleene Algebra with Tests -- 1 Introduction -- 2 Semirings and Weighted Structures -- 3 Weighted Kleene Algebra with Tests -- 3.1 Kleene Algebras -- 3.2 Kleene Algebras with Tests -- 3.3 Weighted Programs -- 4 Language Completeness -- 4.1 Guarded Strings -- 4.2 The Language Completeness Result -- 5 Relational Completeness -- 5.1 Transition Systems -- 5.2 The Relational Completeness Result -- 6 Conclusion -- A Technical appendix -- A.1 Proof of Lemma 2 -- A.2 Proof of ; Theorem 3 -- References -- Modal Hyperdoctrine: Higher-Order and Non-normal Extensions -- 1 Introduction -- 2 Hyperdoctrine Semantics -- 3 Typed First-Order Non-normal Modal Logic -- 3.1 Term Calculus -- 3.2 Logical Calculus -- 4 Hyperdoctrine Semantics for TFOL + EX -- 4.1 Modal Hyperdoctrine Semantics -- 4.2 Soundness and Completeness -- 4.3 Hyperdoctrinal Translation Theorem for TFOL + S4.; 5 Higher-Order Modal Hyperdoctrine -- 5.1 Higher-Order Modal Logic -- 5.2 Modal Tripos -- 5.3 Soundness and Completeness -- 6 Conclusion -- A Soundness of Modal Hyperdoctrine Semantics -- B Completeness of Modal Hyperdoctrine Semantics -- References -- Validity in Contexts -- 1 Introduction -- 2 McGee's Semantics and Three Forms of Inferences -- 2.1 McGee's Semantics -- 2.2 Three Forms of Inferences -- 3 A New Language and Semantics -- 3.1 Problems of McGee's Semantics -- 3.2 A New Language -- 3.3 A New Semantics -- 3.4 Semantic Properties -- 4 Applications -- 4.1 Modus Ponens -- 4.2 Or-to-If -- 4.3 Conditional Proof -- 4.4 Moore Sentences -- 4.5 Conditional Excluded Middle -- 4.6 Infelicitous Statements Involving Conditionals -- 5 Conclusion and Future Work -- References -- Logical Expressibility of Syntactic NL for Complementarity and Maximization -- 1 Background and Main Contributions -- 1.1 Motivational Discussion on Syntactic NL -- 1.2 Major Contributions -- 2 Basic Notions and Notation -- 2.1 Numbers, Machines, and Reducibility -- 2.2 Syntactic NL (or SNL) -- 3 Structural Properties of SNL -- 3.1 Basic Closure Properties and L-m-Reductions -- 3.2 Complementary Problems and SNL -- 4 Maximal SNL (or MAXSNL) -- 5 Brief Conclusion and Open Questions -- References -- Polyadic Quantifiers on Dependent Types -- 1 Introduction -- 1.1 Dependent Types -- 1.2 Polyadic Quantifiers -- 1.3 Polyadic Quantifiers on Dependent Types -- 1.4 Previous Work -- 2 Fibrations -- 2.1 Basic Fibration of a Topos -- 2.2 Cartesian Monads over a Topos -- 3 Strengths on a Cartesian Monad -- 3.1 Strength -- 3.2 Right Strength -- 3.3 Left Strength -- 3.4 Pile'up -- 3.5 Case Study: Continuation Monad on the Fundamental Fibration of Set -- 4 Conclusion -- References -- Author Index.