LEADER 06890nam 22007095 450 001 996465523403316 005 20200705165614.0 010 $a3-540-45620-1 024 7 $a10.1007/3-540-45620-1 035 $a(CKB)1000000000211972 035 $a(SSID)ssj0000321535 035 $a(PQKBManifestationID)11232825 035 $a(PQKBTitleCode)TC0000321535 035 $a(PQKBWorkID)10280288 035 $a(PQKB)11038609 035 $a(DE-He213)978-3-540-45620-9 035 $a(MiAaPQ)EBC3072742 035 $a(PPN)155237160 035 $a(EXLCZ)991000000000211972 100 $a20121227d2002 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aAutomated Deduction - CADE-18$b[electronic resource] $e18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 Proceedings /$fedited by Andrei Voronkov 205 $a1st ed. 2002. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2002. 215 $a1 online resource (XII, 540 p.) 225 1 $aLecture Notes in Artificial Intelligence ;$v2392 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-43931-5 320 $aIncludes bibliographical references and index. 327 $aDescription Logics and Semantic Web -- Reasoning with Expressive Description Logics: Theory and Practice -- BDD-Based Decision Procedures for -- Proof-Carrying Code and Compiler Verification -- Temporal Logic for Proof-Carrying Code -- A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code -- Formal Verification of a Java Compiler in Isabelle -- Non-classical Logics -- Embedding Lax Logic into Intuitionistic Logic -- Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic -- Connection-Based Proof Search in Propositional BI Logic -- System Descriptions -- DDDLIB: A Library for Solving Quantified Difference Inequalities -- An LCF-Style Interface between HOL and First-Order Logic -- System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning -- Proof Development with ?mega -- Learn?matic: System Description -- HyLoRes 1.0: Direct Resolution for Hybrid Logics -- SAT -- Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points -- A Note on Symmetry Heuristics in SEM -- A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions -- Model Generation -- Deductive Search for Errors in Free Data Type Specifications Using Model Generation -- Reasoning by Symmetry and Function Ordering in Finite Model Generation -- Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations -- Session 7 -- A New Clausal Class Decidable by Hyperresolution -- CASC -- Spass Version 2.0 -- System Description: GrAnDe 1.0 -- The HR Program for Theorem Generation -- AutoBayes/CC ? Combining Program Synthesis with Automatic Code Certification ? System Description ? -- CADE-CAV Invited Talk -- The Quest for Efficient Boolean Satisfiability Solvers -- Session 9 -- Recursive Path Orderings Can Be Context-Sensitive -- Combination of Decision Procedures -- Shostak Light -- Formal Verification of a Combination Decision Procedure -- Combining Multisets with Integers -- Logical Frameworks -- The Reflection Theorem: A Study in Meta-theoretic Reasoning -- Faster Proof Checking in the Edinburgh Logical Framework -- Solving for Set Variables in Higher-Order Theorem Proving -- Model Checking -- The Complexity of the Graded ?-Calculus -- Lazy Theorem Proving for Bounded Model Checking over Infinite Domains -- Equational Reasoning -- Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation -- Basic Syntactic Mutation -- The Next Waldmeister Loop -- Proof Theory -- Focussing Proof-Net Construction as a Middleware Paradigm -- Proof Analysis by Resolution. 330 $aThe First CADE in the Third Millennium This volume contains the papers presented at the Eighteenth International C- ference on Automated Deduction (CADE-18) held on July 27?30th, 2002, at the University of Copenhagen as part of the Federated Logic Conference (FLoC 2002). Despite a large number of deduction-related conferences springing into existence at the end of the last millennium, the CADE conferences continue to be the major forum for the presentation of new research in all aspects of automated deduction. CADE-18 was sponsored by the Association for Auto- ted Reasoning, CADE Inc., the Department of Computer Science at Chalmers University, the Gesellschaft fur ¨ Informatik, Safelogic AB, and the University of Koblenz-Landau. There were 70 submissions, including 60 regular papers and 10 system - scriptions. Each submission was reviewed by at least ?ve program committee members and an electronic program committee meeting was held via the Int- net. The committee decided to accept 27 regular papers and 9 system descr- tions. One paper switched its category after refereeing, thus the total number of system descriptions in this volume is 10. In addition to the refereed papers, this volume contains an extended abstract of the CADE invited talk by Ian Horrocks, the joint CADE/CAV invited talk by Sharad Malik, and the joint CADE-TABLEAUX invited talk by Matthias Baaz. One more invited lecture was given by Daniel Jackson. 410 0$aLecture Notes in Artificial Intelligence ;$v2392 606 $aArtificial intelligence 606 $aMathematical logic 606 $aComputer logic 606 $aProgramming languages (Electronic computers) 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 615 0$aArtificial intelligence. 615 0$aMathematical logic. 615 0$aComputer logic. 615 0$aProgramming languages (Electronic computers). 615 14$aArtificial Intelligence. 615 24$aMathematical Logic and Formal Languages. 615 24$aLogics and Meanings of Programs. 615 24$aProgramming Languages, Compilers, Interpreters. 676 $a006.3/33 702 $aVoronkov$b Andrei$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aInternational Conference on Automated Deduction 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996465523403316 996 $aAutomated Deduction - CADE-18$92179789 997 $aUNISA LEADER 03817nam 2200745 450 001 9910797799003321 005 20230807193333.0 010 $a3-11-042460-6 010 $a3-11-042442-8 024 7 $a10.1515/9783110424423 035 $a(CKB)3710000000480572 035 $a(EBL)4001570 035 $a(SSID)ssj0001543282 035 $a(PQKBManifestationID)16134816 035 $a(PQKBTitleCode)TC0001543282 035 $a(PQKBWorkID)14665851 035 $a(PQKB)10157998 035 $a(MiAaPQ)EBC4001570 035 $a(DE-B1597)451933 035 $a(OCoLC)920822711 035 $a(OCoLC)952787521 035 $a(DE-B1597)9783110424423 035 $a(Au-PeEL)EBL4001570 035 $a(CaPaEBR)ebr11129570 035 $a(CaONFJC)MIL828077 035 $a(OCoLC)935243098 035 $a(EXLCZ)993710000000480572 100 $a20160106h20152015 uy 0 101 0 $aeng 135 $aurnnu---|u||u 181 $ctxt 182 $cc 183 $acr 200 10$aIrony and the logic of modernity /$fArmen Avanessian ; translated by Nils F. Schott 210 1$aBerlin, [Germany] ;$aBoston, [Massachusetts] :$cDe Gruyter,$d2015. 210 4$dİ2015 215 $a1 online resource (238 p.) 225 1 $aParadigms : Literature and the Human Sciences,$x2195-2205 ;$vVolume 3 300 $aDescription based upon print version of record. 311 $a3-11-030220-9 320 $aIncludes bibliographical references and index. 327 $tFront matter --$tContents --$tIntroduction --$tPart One: Rhetorologies --$tIntroduction --$t1. Successful Reconciliation --$t2. A Desire for Art --$t3. Mad Consciousness --$tPart Two: Ethica --$tIntroduction --$t1. The Irony of Evil --$t2. Must We Aestheticize? --$t3. Masking Irony --$t4. The Melancholic Subject --$t5. The Joy of Dissimulation --$tPart Three: Novel - Modernity - Irony --$tIntroduction --$t1. The Philosophy of History and the Poetics of Genre --$t2. The Language of the Novel --$t3. From Micro-irony (Quotation) to Macro-irony (Genre) --$t4. Novels of (De)formation and Ironic Autobiographies --$tPart Four: Ironic Politics --$tIntroduction --$t1. The Struggle with Irony --$t2. Thesis and Antithesis --$t3. The Irony of the Law (Kafka and Deleuze ) --$tBibliography --$tIndex 330 $aThe logic of modernity is an ironical logic. Modern irony, a flash of genius produced by Romantic theorists, is first discussed, e.g. in Hegel and Kierkegaard, as an ethical problem personified in figures such as the aesthete, the seducer, the flaneur, or the dandy. It fully develops in the novel, the modern genre par excellence: in novels of the early 19th century no less than in those of postmodernity or in those of the masters of citation, parody, and pastiche of classical modernism (Musil, Joyce, and Proust). This book, however, goes one step further. Looking at how such different authors as Schmitt, Kafka, and Rorty identify the political conflicts, contradictions, and paradoxes of the 20th century as ironical and offers a comprehensive account of the constitutive irony of modernity's ethical, poetical, and political logic. 410 0$aParadigms (Walter de Gruyter & Co.) ;$vVolume 3. 606 $aIrony in literature 606 $aIrony 606 $aModernism (Literature) 610 $aIrony. 610 $amodernity. 610 $apoetics. 610 $apolitics. 615 0$aIrony in literature. 615 0$aIrony. 615 0$aModernism (Literature) 676 $a809.918 686 $aEC 3935$2rvk 700 $aAvanessian$b Armen$01558505 702 $aSchott$b Nils F. 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910797799003321 996 $aIrony and the logic of modernity$93822959 997 $aUNINA