Logical foundations of computer science : international symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10-13, 2022 : proceedings / / Sergei Artemov and Anil Nerode

• Autore: Artemov Sergei
• Pubblicazione: Cham, Switzerland : , : Springer International Publishing, , [2021]; ©2021
• Descrizione fisica: 1 online resource (386 pages)
• Disciplina: 005.1015113
• Soggetto topico: Computer logic; Computer science - Research; Lògica informàtica
• Soggetto genere / forma: Congressos; Llibres electrònics
• Persona (resp. second.): NerodeAnil
• Nota di contenuto: Intro -- 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.
• Titolo autorizzato: Logical foundations of computer science
• ISBN: 3-030-93100-5
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910522937403321
• Lo trovi qui: Univ. Federico II
• Serie: Lecture Notes in Computer Science