001443301 000__ 07079cam\a2200757\i\4500 001443301 001__ 1443301 001443301 003__ OCoLC 001443301 005__ 20230310003537.0 001443301 006__ m\\\\\o\\d\\\\\\\\ 001443301 007__ cr\un\nnnunnun 001443301 008__ 211217s2022\\\\sz\a\\\\o\\\\\101\0\eng\d 001443301 019__ $$a1289364996$$a1289369779$$a1289443541$$a1289480833$$a1294352437 001443301 020__ $$a9783030931001$$q(electronic bk.) 001443301 020__ $$a3030931005$$q(electronic bk.) 001443301 020__ $$z9783030930998 001443301 020__ $$z3030930998 001443301 0247_ $$a10.1007/978-3-030-93100-1$$2doi 001443301 035__ $$aSP(OCoLC)1289341863 001443301 040__ $$aYDX$$beng$$erda$$epn$$cYDX$$dGW5XE$$dEBLCP$$dOCLCF$$dOCLCO$$dDCT$$dOCLCQ$$dOCLCO$$dSFB$$dOCLCQ 001443301 049__ $$aISEA 001443301 050_4 $$aQA75.5$$b.L43 2022 001443301 08204 $$a004$$223 001443301 1112_ $$aLFCS (Symposium)$$d(2022 :$$cDeerfield Beach, Fla.) 001443301 24510 $$aLogical foundations of computer science :$$binternational symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10-13, 2022 : proceedings /$$cSergei Artemov, Anil Nerode (eds.). 001443301 24630 $$aLFCS 2022 001443301 264_1 $$aCham :$$bSpringer,$$c[2022] 001443301 264_4 $$c©2022 001443301 300__ $$a1 online resource :$$billustrations (some color) 001443301 336__ $$atext$$btxt$$2rdacontent 001443301 337__ $$acomputer$$bc$$2rdamedia 001443301 338__ $$aonline resource$$bcr$$2rdacarrier 001443301 347__ $$atext file 001443301 347__ $$bPDF 001443301 4901_ $$aLecture notes in computer science ;$$v13137 001443301 4901_ $$aLNCS sublibrary: SL1 - Theoretical computer science and general issues 001443301 500__ $$aInternational conference proceedings. 001443301 500__ $$aIncludes author index. 001443301 504__ $$aReferences-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. 001443301 5050_ $$aIntro -- 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 001443301 5058_ $$a3 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 001443301 5058_ $$a5 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 001443301 5058_ $$a7.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 001443301 506__ $$aAccess limited to authorized users. 001443301 520__ $$aThis book constitutes the refereed proceedings of the International Symposium on Logical Foundations of Computer Science, LFCS 2022, held in Deerfield Beach, FL, USA, in January 2022. The 23 revised full papers were carefully reviewed and selected from 35 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. 001443301 588__ $$aOnline resource; title from PDF title page (SpringerLink, viewed December 22, 2021). 001443301 650_0 $$aComputer science$$vCongresses. 001443301 650_0 $$aComputer logic$$vCongresses. 001443301 650_6 $$aInformatique$$vCongrès. 001443301 650_6 $$aLogique informatique$$vCongrès. 001443301 655_7 $$aConference papers and proceedings.$$2fast$$0(OCoLC)fst01423772 001443301 655_7 $$aConference papers and proceedings.$$2lcgft 001443301 655_7 $$aActes de congrès.$$2rvmgf 001443301 655_7 $$aCongressos.$$2thub 001443301 655_7 $$aLlibres electrònics.$$2thub 001443301 655_0 $$aElectronic books. 001443301 7001_ $$aArtemov, S. N.,$$eeditor. 001443301 7001_ $$aNerode, Anil,$$d1932-$$eeditor. 001443301 77608 $$iPrint version:$$aLFCS (Symposium) (2022 : Deerfield Beach, Fla.).$$tLogical foundations of computer science.$$dCham : Springer, [2022]$$z3030930998$$z9783030930998$$w(OCoLC)1285551316 001443301 830_0 $$aLecture notes in computer science ;$$v13137. 001443301 830_0 $$aLNCS sublibrary.$$nSL 1,$$pTheoretical computer science and general issues. 001443301 852__ $$bebk 001443301 85640 $$3Springer Nature$$uhttps://univsouthin.idm.oclc.org/login?url=https://link.springer.com/10.1007/978-3-030-93100-1$$zOnline Access$$91397441.1 001443301 909CO $$ooai:library.usi.edu:1443301$$pGLOBAL_SET 001443301 980__ $$aBIB 001443301 980__ $$aEBOOK 001443301 982__ $$aEbook 001443301 983__ $$aOnline 001443301 994__ $$a92$$bISE