Logical Foundations of Computer Science: International Symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10–13, 2022, Proceedings

Preface
Organization
Contents
A Non-hyperarithmetical Gödel Logic
	1 Introduction
	2 Preliminaries
	3 Standard Models via Vagueness
	4 Satisfiability in G"3223379
	5 Validity in G"3223379
	6 Concluding Remarks
	References
Andrews Skolemization May Shorten Resolution Proofs Non-elementarily
	1 Introduction
	2 The Sequent Calculi LK, LK+ and LK++
	3 Skolemization and Deskolemization
	4 Cut-Free LK-Proofs with Weak Quantifiers and Resolution
	5 Andrews Skolemizations Allows for Non-elementarily Shorter Resolution Refutations
	6 Conclusion
	References
The Isomorphism Problem for FST Injection Structures
	1 Introduction and Preliminaries
	2 The Isomorphism Problem for FST Injection Structures
	3 Conclusions and Further Research
	References
Justification Logic and Type Theory as Formalizations of Intuitionistic Propositional Logic
	1 Introduction
		1.1 The BHK Interpretation and Its Formalizations
	2 Justification Logic
		2.1 Substitution
	3 Comparing Formalizations
		3.1 Comparing Proofs
	4 Conclusion
	References
Hyperarithmetical Worm Battles
	1 Introduction
	2 Preliminaries
	3 Arithmetical Soundness of GLP
	4 Worm Battles Outside PA
		4.1 The Reduction Property
		4.2 From 1-consistency to the Worm Principle
		4.3 From the Worm Principle to 1-consistency
	5 Concluding Remarks
	References
Parametric Church's Thesis: Synthetic Computability Without Choice
	1 Preliminaries
		1.1 Common Definitions in CIC
		1.2 Partial Functions
		1.3 The Universe of Propositions P, Elimination, and Choice Principles
		1.4 Notions of Synthetic Computability
	2 Church's Thesis
	3 Synthetic Church's Thesis
	4 Variations of Synthetic Church's Thesis
	5 The Enumerability Axiom
	6 Rice's Theorem
	7 [def:CT]CT in the Weak Call-by-Value -Calculus
	8 Related Work
	A  Consistency and Admissibility of CT in CIC
	References
Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic
	1 Introduction
	2 Preliminaries
	3 Basic Intuitionistic Epistemic Logic
	4 Cut-Free Sequent Calculus
	5 Decidability via Proof Search
	6 Constructive Completeness
		6.1 Lindenbaum Extension
		6.2 Canonical Models
		6.3 Finite Model Property
		6.4 Semantic Cut-Elimination
	7 Completeness for Infinite Theories
		7.1 Arbitrary Theories
		7.2 Enumerable Theories
	8 Conclusion
		8.1 Related Work
		8.2 Future Work
	1  Natural Deduction System for IEL
	2  Coq Mechanisation
		2.1 The Classical Modal Logic K
		2.2 Height-Encoding
	3  Cut-Elimination: Selected Cases
	References
A Parametrized Family of Tversky Metrics Connecting the Jaccard Distance to an Analogue of the Normalized Information Distance
	1 Introduction
	2 Results
	3 Application to Phylogeny
	4 Conclusion
	References
A Parameterized View on the Complexity of Dependence Logic
	1 Introduction
	2 Preliminaries
	3 Complexity Results
		3.1 Data Complexity (dc)
		3.2 Expression and Combined Complexity (ec, cc)
	4 Conclusion
	References
A Logic of Interactive Proofs
	1 Introduction
	2 Syntax
	3 Semantics
	4 Properties and Results
	5 Conclusion
	References
Recursive Rules with Aggregation: A Simple Unified Semantics
	1 Introduction
	2 Problem and Solution Overview
	3 Language
	4 Formal Semantics
		4.1 Interpretations and Derivability
		4.2 Founded Semantics Without Closed Declarations
		4.3 Founded Semantics with Closed Declarations
		4.4 Constraint Semantics
		4.5 Properties of the Semantics
	5 Examples: Company Control and Double Win
		5.1 Company Control—A Well-Known Challenge
		5.2 Double-Win Game—For Any Kind of Moves
		5.3 Experiments
	6 Related Work and Conclusion
	References
Computational Properties of Partial Non-deterministic Matrices and Their Logics
	1 Introduction
	2 Warming Up
	3 Checking Theorem Universality
		3.1 Computing Total Components
		3.2 Determining the Existence of Non-theorems
	4 Checking Theorem Existence
		4.1 A Bridge with (Term-DAG) Automata
	5 Deciding Equality of Theoremhood
	6 Conclusions and Further Work
	References
Soundness and Completeness Results for LEA and Probability Semantics
	1 Introduction
		1.1 Overview of the Logic of Evidence Aggregation
		1.2 LEA Definition
		1.3 Alternative Formulation of LEA
		1.4 Probability Semantics Definition
	2 Sound and Complete Semantics for LEA
		2.1 Basic Models
		2.2 Deductive Basic Models
	3 Sound and Complete Axiomatization of Probability Semantics
		3.1 LEA- Definition and Models
		3.2 More LEA- Results
		3.3 LEA+ Definition and Basic Results
		3.4 Basic Models of LEA+
		3.5 Probability Semantics for LEA+
	4 Further Discussion
		4.1 Decidability Results
		4.2 Justification Logic as Propositional Logic
		4.3 Future Research
	References
On Inverse Operators in Dynamic Epistemic Logic
	1 Introduction
	2 A General Framework for DEL
		2.1 Syntax
		2.2 Semantics
	3 Inverse Operators
		3.1 Introduction of Inverse Operators
		3.2 Completeness
		3.3 Irreducibility
		3.4 Conservativity
	4 Categorical Construction of Model Transition Systems
	5 Related Work
	6 Conclusion and Future Work
	References
Betwixt Turing and Kleene
	1 Introduction: Jordan, Turing, and Kleene
	2 Preliminaries
		2.1 Kleene's Higher-Order Computability Theory
		2.2 Some Higher-Order Notions
	3 Main Results
		3.1 Jordan Realisers and Equivalent Formulations
		3.2 Jordan Realisers and Countable Sets
		3.3 Computing Kleene's 3 from Jordan Realisers
		3.4 Jordan Realisers and the Uncountability of R
	References
Computability Models over Categories and Presheaves
	1 Introduction
	2 Computability Models
	3 Total Computability Models over Categories
	4 Partial Models over Categories with Pullbacks
	5 Categories with a Base of Computability
	6 Concluding Comments and Future Work
	References
Reducts of Relation Algebras: The Aspects of Axiomatisability and Finite Representability
	1 Introduction
	2 Definitions
		2.1 Relation Algebras and Their Reducts
		2.2 Residuated Semigroups
		2.3 Join Semilattice-Ordered Semigroups
		2.4 Order-theoretic Definitions
		2.5 Pseudo-elementary Classes
	3 The Finite Representation Property for Residuated Semigroups
	4 Join Semilattice-Ordered Semigroups: The Explicit Axiomatisation
	References
Between Turing and Kleene
	1 Between Turing and Kleene Computability
		1.1 Short Summary
		1.2 Extending the Scope of Turing Computability
		1.3 The Need for an Extension of Turing Computation
	2 Some Results
		2.1 Nets and Computability Theory
		2.2 On the Uncountability of R
		2.3 Discontinuous Functions
	References
Propositional Dynamic Logic with Quantification over Regular Computation Sequences
	1 Introduction
	2 Regular Computation Sequences
	3 QPDL and Its ĭ䘀爀攀攀 䘀爀愀最洀攀渀琀 焀倀䐀䰀
	4 Expressivity
		4.1 Expressing Acceptance Properties of NFA
		4.2 Ways to Execute a Plan Successfully
	5 Decidability and Complexity of qPDL
		5.1 DPDL
		5.2 An Embedding of qPDL into DPDL
	6 Discussion
	7 Conclusion
	References
Finite Generation and Presentation Problems for Lambda Calculus and Combinatory Logic
	1 Introduction
	2 Finite Generation
	3 Finite Presentation
	References
Exact and Parameterized Algorithms for Read-Once Refutations in Horn Constraint Systems
	1 Introduction
	2 Statement of Problems
	3 Motivation and Related Work
	4 A Parameterized Algorithm
		4.1 Correctness
		4.2 Resource Analysis
	5 An Exact Exponential Algorithm
		5.1 Resource Analysis
	6 Literal-Once Refutations
	7 A Lower Bound on Kernel Size
	8 Conclusion
	References
Dialectica Logical Principles
	1 Introduction
	2 Logical Principles in the Dialectica Interpretation
		2.1 Independence of Premise
		2.2 Markov's Principle
	3 Logical Doctrines
	4 Logical Principles via Universal Properties
	5 Logical Principles in Gödel Hyperdoctrines
	6 Conclusion
	References
Small Model Property Reflects in Games and Automata
	1 Introduction
	2 Preliminaries
		2.1 Models
		2.2 The Finite Model Property and the Small Model Property
	3 Small Model Size and Small Afrodite Strategies
		3.1 Better Variables
		3.2 Construction of the Strategy
	4 Small Model Size and the Arcadian Automata
		4.1 Arcadian Automata
		4.2 Better Variables in Arcadian Automata
		4.3 Loquacious Runs
	5 Conclusion
	References
Author Index