Logical Foundations of Computer Science: International Symposium, LFCS 2020, Deerfield Beach, FL, USA, January 4–7, 2020, Proceedings (Lecture Notes in Computer Science Book 11972)

This book constitutes the refereed proceedings of the International Symposium on Logical Foundations of Computer Science, LFCS 2020, held in Deerfield Beach, FL, USA, in January 2020. The 17 revised full papers were carefully reviewed and selected from 30 submissions. The scope of the Symposium is broad and includes constructive mathematics and type theory; homotopy type theory; logic, automata, and automatic structures; computability and randomness; logical foundations of programming; logical aspects of computational complexity; parameterized complexity; logic programming and constraints; automated deduction and interactive theorem proving; logical methods in protocol and program verification; logical methods in program specification and extraction; domain theory logics; logical foundations of database theory; equational logic and term rewriting; lambda and combinatory calculi; categorical logic and topological semantics; linear logic; epistemic and temporal logics; intelligent and multiple-agent system logics; logics of proof and justification; non-monotonic reasoning; logic in game theory and social software; logic of hybrid systems; distributed system logics; mathematical fuzzy logic; system design logics; other logics in computer science.-- Provided by publisher Preface......Page 6 Organization......Page 7 Contents......Page 9 1 Introduction......Page 11 1.1 Preliminaries......Page 12 3 Lower Bounds for Quantifier-Free Formulas......Page 15 4 Boolean Combinations of n-Formulas......Page 18 References......Page 21 1 Preliminaries......Page 22 1.1 Motivations......Page 23 2 Observable Models......Page 24 3 On the Structure of Induced Observable Models......Page 25 4 Derivations from Hypotheses in Modal Logic......Page 26 5 Canonical Models for S5 with a single letter......Page 27 6 From Observable Models to Kripke Models......Page 29 7.1 Common Knowledge and Necessitation......Page 30 7.2 Canonical Models of Sets of Assumptions......Page 31 8.1 Ignorant Agent Example......Page 33 9 Intuitionistic Observable Models......Page 34 10 Findings and Suggestions......Page 35 References......Page 36 1 Introduction......Page 37 2 Non-normal Modal Logics......Page 39 3 Hypersequent Calculi......Page 41 4 Complexity of Proof Search......Page 44 5 Countermodel Extraction......Page 46 6 Extensions with Axioms T, P, and D......Page 50 7 Conclusion......Page 52 References......Page 56 1 Introduction......Page 57 2 Syntax, Deduction, Computability......Page 59 2.2 Deduction Systems......Page 60 2.3 Synthetic Computability......Page 61 3.1 Tarski Semantics......Page 62 3.2 Kripke Semantics......Page 66 4 On Markov's Principle......Page 70 5 Algebraic Semantics......Page 72 6 Game Semantics......Page 74 7 Discussion......Page 75 7.2 Future Work......Page 76 A Overview of Deduction Systems......Page 77 B Notes on the Coq Formalisation......Page 78 References......Page 81 1 Introduction......Page 85 2 The Constant Sentences of Peano Arithmetic......Page 86 3 Generalized `Constructive' Liar Sentences and Rosser Sentences......Page 89 4 `Extremely' Independent Sentences......Page 92 5 Concluding Remark......Page 93 References......Page 94 1 Introduction......Page 95 2 Syntax......Page 97 3 Semantics......Page 99 4 Soundness......Page 103 5 Basic Properties......Page 104 References......Page 106 1 Introduction......Page 108 2.1 Finite Partial Functions......Page 109 2.3 Basic-Terms and Accessibility......Page 110 2.4 A Formal Language......Page 111 2.5 Definable Classes of Fp-Structures......Page 112 3.2 The Theory FST0......Page 113 3.3 Some Derived Schemas......Page 114 4.2 Imperative Programs for Generic PR Computing......Page 116 5 An Abstract Form of Parson's Theorem......Page 118 References......Page 119 1 Introduction......Page 121 2 Need of Easier Programming with Logic......Page 122 3 DA Logic......Page 125 4 Formal Definition of Semantics of DA Logic......Page 128 5 Additional Examples......Page 132 References......Page 135 1 Introduction......Page 138 2 The Derivation of First-Order Rules from Second-Order Rule Macros: A First Approach......Page 140 3 LK++: A Globally Sound Calculus, Cf. aguilera2016unsound......Page 143 4 The Analytic Sequent Calculus LH++......Page 145 5 Soundness, Completeness and Cut-Elimination for LH++......Page 149 References......Page 153 1 Introduction......Page 154 2 Background on O......Page 155 3 Strict Feedback Hyperjump......Page 156 4 Loose Feedback Hyperjump......Page 161 References......Page 165 1 Introduction......Page 166 2 Logical Preliminaries......Page 168 3 Soundness and Completeness of LNIF......Page 171 4 Proof-Theoretic Properties of LNIF......Page 173 5 Conclusion......Page 183 References......Page 184 1 Introduction......Page 187 2.1 The Labelled Calculi G3Int and G3IntQC......Page 189 2.2 The Nested Calculi NInt and NIntQC......Page 191 3 Translating Notation: Labelled and Nested......Page 192 4 Deriving NInt from G3Int......Page 195 5 Deriving NIntQC from G3IntQC......Page 200 6 Conclusion......Page 202 References......Page 203 1 Introduction......Page 205 2 Preliminaries......Page 208 2.1 Base Independence......Page 213 3 Complexity Results for Abductive Reasoning......Page 214 3.2 Parameter `Number of Explanations' |E|......Page 217 3.3 Parameter `Number of Manifestations' |M|......Page 218 4 Conclusion......Page 220 References......Page 221 1 Introduction......Page 224 2 Preliminaries......Page 225 3 The LGPAC......Page 226 4 Tracking Computability......Page 230 5 Computability of the Input-Output Operator......Page 233 6 Computability of LGPAC-Generable Functions......Page 235 7 Some Applications of Theorem 1......Page 238 8 Discussion......Page 240 References......Page 244 1 Introduction......Page 246 2 Motivation......Page 247 3 Typed Lambda-Calculus Based on IEL-......Page 250 4 Relation with the Monadic Metalanguage......Page 255 References......Page 257 1 Introduction......Page 259 2.1 Reverse Mathematics......Page 260 2.2 Some Axioms of Higher-Order RM......Page 263 3.1 Specker Nets......Page 264 3.2 Compactness of Metric Spaces......Page 268 3.3 Rado Selection Lemma......Page 271 3.4 Fields and Order......Page 272 4.2 Implications and Interpretations......Page 274 References......Page 276 1 Introduction......Page 278 2 Revisiting Some Intuitions of Gödel and Hilbert......Page 280 3 Main Notation and Background Literature......Page 281 4 Main Theorems and Related Notation......Page 284 5 Intuition Behind Theorem 1......Page 287 6 Summary of the Justification For Theorem 2......Page 289 7 On the Significance of Theorems 1 and 2......Page 290 References......Page 294 Author Index......Page 297 This book constitutes the refereed proceedings of the International Symposium on Logical Foundations of Computer Science, LFCS 2013, held in San Diego, CA, USA in January 2013. The volume presents 29 revised refereed papers carefully selected by the program committee. The scope of the Symposium is broad and includes constructive mathematics and type theory; logic, automata and automatic structures; computability and randomness; logical foundations of programming; logical aspects of computational complexity; logic programming and constraints; automated deduction and interactive theorem proving; logical methods in protocol and program verification; logical methods in program specification and extraction; domain theory logic; logical foundations of database theory; equational logic and term rewriting; lambda and combinatory calculi; categorical logic and topological semantics; linear logic; epistemic and temporal logics; intelligent and multiple agent system logics; logics of proof and justification; nonmonotonic reasoning; logic in game theory and social software; logic of hybrid systems; distributed system logics; mathematical fuzzy logic; system design logics; and other logics in computer science.