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 Theif'' 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