Logical Foundations of Computer Science

1. Front Matter

   Pages i-x

   PDF

2. Computability of Algebraic and Definable Closure

   • Nathanael Ackerman, Cameron Freer, Rehana Patel

   Pages 1-11

3. Observable Models

   • Sergei Artemov

   Pages 12-26

4. Countermodel Construction via Optimal Hypersequent Calculi for Non-normal Modal Logics

   • Tiziano Dalmonte, Björn Lellmann, Nicola Olivetti, Elaine Pimentel

   Pages 27-46

5. Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory

   • Yannick Forster, Dominik Kirst, Dominik Wehr

   Pages 47-74

6. On the Constructive Truth and Falsity in Peano Arithmetic

   • Hirohiko Kushida

   Pages 75-84

7. Belief Expansion in Subset Models

   • Eveline Lehmann, Thomas Studer

   Pages 85-97

8. Finitism, Imperative Programs and Primitive Recursion

   • Daniel Leivant

   Pages 98-110

9. Knowledge of Uncertain Worlds: Programming with Logical Constraints

   • Yanhong A. Liu, Scott D. Stoller

   Pages 111-127

10. A Globally Sound Analytic Calculus for Henkin Quantifiers

    • Matthias Baaz, Anela Lolic

    Pages 128-143

11. Feedback Hyperjump

    • Robert S. Lubarsky

    Pages 144-155

12. Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents

    • Tim Lyon

    Pages 156-176

13. On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems

    • Tim Lyon

    Pages 177-194

14. Parameterised Complexity of Abduction in Schaefer’s Framework

    • Yasir Mahmood, Arne Meier, Johannes Schmidt

    Pages 195-213

15. Tracking Computability of GPAC-Generable Functions

    • Diogo Poças, Jeffery Zucker

    Pages 214-235

16. Modal Type Theory Based on the Intuitionistic Modal Logic \(\mathbf{IEL}^{-}\)

    • Daniel Rogozin

    Pages 236-248

17. Lifting Recursive Counterexamples to Higher-Order Arithmetic

    • Sam Sanders

    Pages 249-267

18. On the Tender Line Separating Generalizations and Boundary-Case Exceptions for the Second Incompleteness Theorem Under Semantic Tableaux Deduction

    • Dan E. Willard

    Pages 268-286

19. Back Matter

    Pages 287-287

    PDF

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.

• artificial intelligence
• complexity
• computability
• computer science
• constructive type theory
• first-order logic
• formal logic
• GPAC-generable functions
• highre-order arithmetics
• knowledge of uncertain worlds
• modal logic
• non-normal modal logics
• observable models
• primitive recursion
• problem solving
• semanitic systems
• theorem proving

• The Graduate Center, CUNY, New York, USA

  Sergei Artemov

• Cornell University, Ithaca, USA

  Anil Nerode

Policies and ethics