LEADER 02793nam 2200637Ia 450 001 9910460244503321 005 20200520144314.0 010 $a0-8166-7519-8 035 $a(CKB)2670000000069686 035 $a(EBL)635545 035 $a(OCoLC)699475357 035 $a(SSID)ssj0000528040 035 $a(PQKBManifestationID)11306442 035 $a(PQKBTitleCode)TC0000528040 035 $a(PQKBWorkID)10544934 035 $a(PQKB)10914360 035 $a(MiAaPQ)EBC635545 035 $a(Au-PeEL)EBL635545 035 $a(CaPaEBR)ebr10440586 035 $a(EXLCZ)992670000000069686 100 $a20100804d2010 uy 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 00$aMechademia$h5$iFanthropologies$b[electronic resource] /$fFrenchy Lunning, editor 210 $aMinneapolis, MN $cUniversity of Minnesota Press$d2010 215 $a1 online resource (401 p.) 225 1 $aMechademia ;$vv.v. 5 300 $aDescription based upon print version of record. 311 $a0-8166-7387-X 320 $aIncludes bibliographical references. 327 $aContents; Introduction; Sites of Transposition; Patterns of Consumption; Modes of Circulation; Styles of Intervention; Review and Commentary; Contributors; Call for Papers 330 $aPassionate fans of anime and manga, known in Japan as otaku and active around the world, play a significant role in the creation and interpretation of this pervasive popular culture. Routinely appropriating and remixing favorite characters, narratives, imagery, and settings, otaku take control of the anime characters they consume. Fanthropologies -the fifth volume in the Mechademia series, an annual forum devoted to Japanese anime and manga-focuses on fans, fan activities, and the otaku phenomenon. The zones of activity discussed in these essays range from fan-subs (fan-subtitled versions of a 410 0$aMechademia 606 $aAnimated films$zJapan$xHistory and criticism 606 $aAnimated television programs$zJapan$xHistory and criticism 606 $aComic books, strips, etc$zJapan$xHistory and criticism 606 $aPopular culture$xJapanese influences 606 $aVideo games$zJapan 608 $aElectronic books. 615 0$aAnimated films$xHistory and criticism. 615 0$aAnimated television programs$xHistory and criticism. 615 0$aComic books, strips, etc.$xHistory and criticism. 615 0$aPopular culture$xJapanese influences. 615 0$aVideo games 676 $a741.5095105 701 $aLunning$b Frenchy$0975918 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910460244503321 996 $aMechademia$92447280 997 $aUNINA LEADER 10389nam 2200565 450 001 996464551903316 005 20231110230057.0 010 $a3-030-93100-5 035 $a(MiAaPQ)EBC6827704 035 $a(Au-PeEL)EBL6827704 035 $a(OCoLC)1289369779 035 $a(CKB)20151338900041 035 $a(PPN)259385115 035 $a(EXLCZ)9920151338900041 100 $a20220831d2021 uy 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aLogical foundations of computer science $einternational symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10-13, 2022 : proceedings /$fSergei Artemov and Anil Nerode 210 1$aCham, Switzerland :$cSpringer International Publishing,$d[2021] 210 4$d©2021 215 $a1 online resource (386 pages) 225 1 $aLecture Notes in Computer Science ;$vv.13137 311 08$aPrint version: Artemov, Sergei Logical Foundations of Computer Science Cham : Springer International Publishing AG,c2022 9783030930998 327 $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 -- 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. 327 $aA 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. 327 $a6 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. 327 $a3.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. 327 $a2 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. 410 0$aLecture Notes in Computer Science 606 $aComputer logic$vCongresses 606 $aComputer science$xResearch 606 $aLògica informàtica$2thub 608 $aCongressos$2thub 608 $aLlibres electrònics$2thub 615 0$aComputer logic 615 0$aComputer science$xResearch. 615 7$aLògica informàtica 676 $a005.1015113 700 $aArtemov$b Sergei$01080720 702 $aNerode$b Anil 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996464551903316 996 $aLogical foundations of computer science$92910220 997 $aUNISA