LEADER 02544nam 2200577 450 001 9910453523503321 005 20200520144314.0 010 $a90-272-7070-8 035 $a(CKB)2550000001192249 035 $a(EBL)1605606 035 $a(SSID)ssj0001155257 035 $a(PQKBManifestationID)11651373 035 $a(PQKBTitleCode)TC0001155257 035 $a(PQKBWorkID)11187542 035 $a(PQKB)10492135 035 $a(MiAaPQ)EBC1605606 035 $a(Au-PeEL)EBL1605606 035 $a(CaPaEBR)ebr10833612 035 $a(CaONFJC)MIL572244 035 $a(OCoLC)870088282 035 $a(EXLCZ)992550000001192249 100 $a20140211h20142014 uy| 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 00$aCross-linguistic investigations of nominalization patterns /$fedited by Ileana Paul, University of Western Ontario, London, Ontario 210 1$aAmsterdam :$cJohn Benjamins Publishing Company,$d[2014] 210 4$dİ2014 215 $a1 online resource (231 p.) 225 1 $aLinguistik aktuell,$x0166-0829 ;$vvolume 210 300 $aDescription based upon print version of record. 311 $a90-272-5593-8 311 $a1-306-40993-4 320 $aIncludes bibliographical references and index. 327 $apart 1. Verbal structure inside nominalizations -- part 2. The referent of nominalization -- part 3. The nature of the nominalizer. 330 $aPatterns of nominalization in Blackfoot are surveyed. It is demonstrated that two of these patterns behave like nouns while two others only partially behave like nouns. Degrees of nominality are analyzed within the assumption that there is a universal syntactic spine, a hierarchically organized set of categories, which are not intrinsically specified for nominality or verbality. They are category-neutral. Different nominalization patterns (and degrees of nominality) reduce to different ways of introducing the nominalizer: it may be introduced by a dedicated morphological marker (nominalization 410 0$aLinguistik aktuell ;$vBd. 210. 606 $aGrammar, Comparative and general$xNominals 608 $aElectronic books. 615 0$aGrammar, Comparative and general$xNominals. 676 $a410.367 701 $aPaul$b Ileana$0889409 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910453523503321 996 $aCross-linguistic investigations of nominalization patterns$92199956 997 $aUNINA LEADER 06451nam 22007215 450 001 996418305603316 005 20200703023833.0 010 $a3-030-51054-9 024 7 $a10.1007/978-3-030-51054-1 035 $a(CKB)4100000011325534 035 $a(MiAaPQ)EBC6283192 035 $a(DE-He213)978-3-030-51054-1 035 $a(PPN)248595342 035 $a(EXLCZ)994100000011325534 100 $a20200629d2020 u| 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aAutomated Reasoning$b[electronic resource] $e10th International Joint Conference, IJCAR 2020, Paris, France, July 1?4, 2020, Proceedings, Part II /$fedited by Nicolas Peltier, Viorica Sofronie-Stokkermans 205 $a1st ed. 2020. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2020. 215 $a1 online resource (521 pages) 225 1 $aLecture Notes in Artificial Intelligence ;$v12167 311 $a3-030-51053-0 327 $aInteractive Theorem Proving/ HOL -- Competing inheritance paths in dependent type theory: a case study in functional analysis -- A Lean tactic for normalising ring expressions with exponents (short paper) -- Practical proof search for Coq by type inhabitation -- Quotients of Bounded Natural Functors -- Trakhtenbrot?s Theorem in Coq -- Deep Generation of Coq Lemma Names Using Elaborated Terms -- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs -- Validating Mathematical Structures -- Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description) -- Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages -- Formalizations -- Formalizing the Face Lattice of Polyhedra -- Algebraically Closed Fields in Isabelle/HOL -- Formalization of Forcing in Isabelle/ZF -- Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL -- Formal Proof of the Group Law for Edwards Elliptic Curves -- Verifying Farad_zev-Read type Isomorph-Free Exhaustive Generation -- Verification -- Verified Approximation Algorithms -- Efficient Verified Implementation of Introsort and Pdqsort -- A Fast Verified Liveness Analysis in SSA form -- Verification of Closest Pair of Points Algorithms -- Reasoning Systems and Tools -- A Polymorphic Vampire (short paper) -- N-PAT: A Nested Model-Checker (system description) -- HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description) -- Implementing superposition in iProver (system description) -- Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description) -- Make E Smart Again -- Automatically Proving and Disproving Feasibility Conditions -- µ-term: Verify Termination Properties Automatically (system description) -- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) -- The Imandra Automated Reasoning System (system description) -- A Programmer?s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description) -- Sequoia: a playground for logicians (system description) -- Prolog Technology Reinforcement Learning Prover (system description). 330 $aThis two-volume set LNAI 12166 and 12167 constitutes the refereed proceedings of the 10th International Joint Conference on Automated Reasoning, IJCAR 2020, held in Paris, France, in July 2020.* In 2020, IJCAR was a merger of the following leading events, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), ITP (International Conference on Interactive Theorem Proving), and TABLEAUX (International Conference on Analytic Tableaux and Related Methods). The 46 full research papers, 5 short papers, and 11 system descriptions presented together with two invited talks were carefully reviewed and selected from 150 submissions. The papers focus on the following topics: Part I: SAT; SMT and QBF; decision procedures and combination of theories; superposition; proof procedures; non classical logics Part II: interactive theorem proving/ HOL; formalizations; verification; reasoning systems and tools *The conference was held virtually due to the COVID-19 pandemic. Chapter ?A Fast Verified Liveness Analysis in SSA Form? is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. 410 0$aLecture Notes in Artificial Intelligence ;$v12167 606 $aMathematical logic 606 $aArtificial intelligence 606 $aComputer logic 606 $aSoftware engineering 606 $aProgramming languages (Electronic computers) 606 $aComputer programming 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 615 0$aMathematical logic. 615 0$aArtificial intelligence. 615 0$aComputer logic. 615 0$aSoftware engineering. 615 0$aProgramming languages (Electronic computers). 615 0$aComputer programming. 615 14$aMathematical Logic and Formal Languages. 615 24$aArtificial Intelligence. 615 24$aLogics and Meanings of Programs. 615 24$aSoftware Engineering. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aProgramming Techniques. 676 $a004.015113 702 $aPeltier$b Nicolas$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aSofronie-Stokkermans$b Viorica$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a996418305603316 996 $aAutomated Reasoning$9771895 997 $aUNISA