Logic, language, information, and computation : 27th international workshop, WoLLIC 2021, virtual event, October 5-8, 2021 : proceedings

Preface
Organization
Contents
Formalized Soundness and Completeness of Epistemic Logic
	1 Introduction
	2 Related Work
	3 Syntax and Semantics
	4 Normal Modal Logic
		4.1 Proof System
		4.2 Soundness
		4.3 Derived Rules
	5 Abstract Completeness
		5.1 Maximal Consistent Sets
		5.2 Lindenbaum's Lemma
		5.3 Model Existence
	6 Concrete Systems
		6.1 System K
		6.2 System T
		6.3 Systems KB, K4, S4
	7 System S5
		7.1 Compositional Version
		7.2 Alternative Version
	8 Conclusion and Future Work
	References
A Logical Characterization of Constant-Depth Circuits over the Reals
	1 Introduction
	2 Preliminaries
		2.1 Machines over R
		2.2 Arithmetic Circuits over R
		2.3 R-Structures and First-Order Logic over R
	3 Characterizing AC0
		3.1 A Characterization for Non-uniform AC0
		3.2 Characterizations for UP-AC0
	4 Conclusion
	References
Wanted Dead or Alive: Epistemic Logic for Impure Simplicial Complexes
	1 Introduction
	2 Technical Preliminaries: Simplicial Complexes
	3 Epistemic Logic on Impure Simplicial Models
		3.1 Validities and Differences with the Logic S5
	4 Correspondence to Kripke Models
	5 Bisimulation for Impure Simplicial Complexes
	6 Comparison to the Literature and Further Research
	References
Doubly Strongly First Order Dependencies
	1 Introduction
	2 Preliminaries
		2.1 Team Semantics
		2.2 Strongly First Order Dependencies
		2.3 Relations Definable over the Empty Signature
	3 Doubly Strongly First Order Dependencies
	References
Explicit Non-normal Modal Logic
	1 Introduction
	2 Justification Logic
	3 Neighborhood Semantics and Modular Models
	4 Monotonic Justification Logic
	5 Realisation
	6 Conclusion
	A Soundness and Completeness with Respect to Basic Models
	B Soundness and Completeness with Respect to Modular Models
	C Soundness and Completeness with Respect to Fully Explanatory Modular Models
	References
A General Relational Semantics of Propositional Logic: Axiomatization
	1 Introduction
	2 The Logic PL
		2.1 Formal Language
		2.2 Semantic Consequence
		2.3 Syntactic Consequence
		2.4 Soundness and Completeness
	3 Extensions of PL
		3.1 Intuitionistic Logic
		3.2 Ortho-Logic
	4 Future Work
	A  Intuitionistic Logic
	B  Ortho-logic
	References
Meaning and Computing: Two Approaches to Computable Propositions
	1 Introduction
	2 Constructive Tradition
		2.1 Proofs as Programs
		2.2 Constructive Type Theory
	3 Non-constructive Tradition
		3.1 Transparent Intensional Logic
	4 Conclusion
	References
Modal Logic via Global Consequence
	1 Introduction
	2 Relationship Between Local and Global Consequence
	3 Global Correspondence
	4 Applications
		4.1 Informational Consequence
		4.2 Update Consequence
	5 Conclusions and Future Work
	References
Games for Hybrid Logic
	1 Introduction
	2 Preliminaries
	3 A Game for Truth
	4 A Game for Validity
	5 From Strategies to Proof Systems
		5.1 Your Optimal Choices or How to Achieve Finite Branching
		5.2 The Proof System DS
	6 Conclusion and Future Work
	References
Verifying the Conversion into CNF in Dafny
	1 Introduction
	2 The Textbook Conversion into CNF
		2.1 Data Structures
		2.2 Algorithm
		2.3 Proof of Termination
	3 The Tseitin Conversion
		3.1 Data Structures
		3.2 The Algorithm
		3.3 The Proof
	4 Related Work
	5 Discussion
	A  Short Overview of Dafny
	B  The Dafny Development
	References
Analysis in a Formal Predicative Set Theory
	1 Introduction
	2 Preliminaries
		2.1 Notations
		2.2 The Theory PZF-U
		2.3 Extending the Base Language
		2.4 Basic Notations
		2.5 Mathematics in PZF
		2.6 Recursive Definitions
		2.7 Finite Sums
	3 Sequences of Dedekind Cuts
	4 The Real Line
	5 Continuous Functions
		5.1 Intermediate Value Theorem
	A Appendix
		A.1 Uniformly Convergence and Power Series
		A.2  Elementary Functions
	References
Coherence via Focusing for Symmetric Skew Monoidal Categories
	1 Introduction
	2 Braided/Symmetric Skew Monoidal Categories
	3 The Free Symmetric Skew Monoidal Category
	4 Symmetric Skew Monoidal Sequent Calculus
	5 A Focused Subsystem for the Symmetric Skew Case
	6 Recovering Coherence for the Non-Skew Case
	7 Conclusions and Future Work
	References
On the Subtle Nature of a Simple Logic of the Hide and Seek Game
	1 From Games to Logic
	2 Logic of Hide and Seek (LHS)
	3 Bisimulation and Expressive Power
	4 Towards Undecidability of the Satisfaction Problem
		4.1 Undecidability
	5 Related Works
	6 Conclusion and Future Work
	References
Orthogonal Frames and Indexed Relations
	1 Introduction
	2 Examples of Indexed Frames
	3 Orthogonal Frames
	4 Orthogonal Structures
	5 Some Case Studies
	6 Discussion and Future Work
	References
Computable Execution Traces
	1 Introduction
		1.1 Preliminaries
	2 Finite Control Computability
	3 Carrying Out Trace Sets
		3.1 Expansion Mapping
		3.2 Carrying Out
	4 Further Directions
	A  Technical Appendix
		A.1  Preliminaries
		A.2  Proof of Theorem 2
		A.3  Proof of Theorem 3
	References
Axiomatic Reals and Certified Efficient Exact Real Computation
	1 Introduction
	2 Computable Analysis and Exact Real Computation
	3 Axiomatization
		3.1 Kleenean and Multivalued Lifting
		3.2 Real Numbers
		3.3 Soundness by Realizabiltiy
	4 Relating Classical Analysis
	5 Implementation and Examples
		5.1 Maximization
		5.2 Intermediate Value Theorem (IVT)
		5.3 Classical Proofs and a Fast Square Root Algorithm
		5.4 Performance Measurements
	6 Conclusion and Future Work
	A Full List of Axioms
	B Code Extraction
	References
Lorenzen Won the Game, Lorenz Did Too: Dialogical Logic for Ellipsis and Anaphora Resolution
	1 Introduction
	2 Data
		2.1 Pronouns
		2.2 Ellipsis
	3 Methods
		3.1 Events
		3.2 Categorial Grammar
	4 Dialogical Logic
		4.1 First Order Language
		4.2 Dialogical Games: Informal Overview
		4.3 Argumentation Forms
		4.4 Moves, and Augmented Sequences
		4.5 Games
	5 Discussion
	6 Conclusion
	References
Uniform Lyndon Interpolation for Basic Non-normal Modal Logics
	1 Introduction
	2 Preliminaries
		2.1 Sequent Calculi
	3 Uniform Lyndon Interpolation
		3.1 Modal Logics M and MN
		3.2 Modal Logic MC
		3.3 Modal Logics E and EN
	4 Modal Logics EC and ECN
	References
On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties
	1 Introduction
	2 Preliminaries
	3 Embedding TeamLTL and Its Extensions into First-Order Team Logic
		3.1 Asynchronous Semantics
	4 Asynchronicity and Stutter Equivalence
	5 SO Versus Arithmetic Definability
	6 Complexity of Model Checking and Satisfiability
	7 Conclusion and Future Work
	References
Characterizations for XPathR("3223379 )
	1 Introduction
	2 Preliminaries
	3 Bisimulation and Equivalence
	4 Characterizations
	5 Conclusions and Future Work
	A Proofs and Definitions Omitted from the Main Text
	References
Uniform Interpolation via Nested Sequents
	1 Introduction
	2 Preliminaries
	3 Uniform Interpolation for Nested Sequents
		3.1 Uniform Interpolation For K
		3.2 Uniform Interpolation For D and T
	4 Conclusion
	References
Disjunction and Negation in Information Based Semantics
	1 Introduction
	2 Semilattice Semantics
	3 Incompatibility Relation in Information Frames
	4 Comparison with Hartonas' Approach
	A  Appendix
	References
Algorithmically Broad Languages for Polynomial Time and Space
	1 Introduction
	2 Finite Functions as Generic Data
		2.1 F-Functions
		2.2 Bundles
		2.3 Bundles for Inductive Data
	3 Programs for Bundle Transformation
		3.1 Atomic Operations
		3.2 Programs
		3.3 Functions in BT
		3.4 Examples of BT-programs
	4 Variants and Primitive-Recursive Complexity
		4.1 Recursion with Variants
		4.2 Semantics of BTV
		4.3 Examples of BTV-programs
	5 Ramification
		5.1 The Ramification Method
		5.2 Ramified Imperative Recursion
		5.3 Related Work in Static Analysis
	6 Completeness and Soundness Properties
		6.1 Extensional Completeness of BTR* for PTime
		6.2 Soundness of BTR and BTR* for Feasibility
	7 Examples of BTR*-programs
		7.1 Fundamental Examples
		7.2 Limitative Examples
	8 Conclusion and Directions
	References
A Pure View of Ecumenical Modalities
	1 Introduction
	2 Preliminaries
		2.1 Ecumenical Birelational Models
	3 A Nested System for Ecumenical Modal Logic
		3.1 Harmony
	4 Soundness
	5 Completeness
	6 Extracting Fragments
	7 Extensions
	8 Conclusion
	References
Provability Games for Non-classical Logics
	1 Introduction
	2 Game for Minimal Logic
	3 Game for Modal Logic
		3.1 Mezhirov Game for Modal Logic of Functional Frames
		3.2 Mezhirov Game for Modal Logic of Serial Frames
	4 Conclusion and Future Work
	References
Author Index