LEADER 07614nam 2200721Ia 450 001 9910953334403321 005 20200520144314.0 010 $a9786613092441 010 $a9781283092449 010 $a1283092441 010 $a9789027285386 010 $a9027285381 024 7 $a10.1075/cilt.254 035 $a(CKB)2550000000033080 035 $a(SSID)ssj0000473521 035 $a(PQKBManifestationID)11286592 035 $a(PQKBTitleCode)TC0000473521 035 $a(PQKBWorkID)10449423 035 $a(PQKB)10180422 035 $a(MiAaPQ)EBC680960 035 $a(Au-PeEL)EBL680960 035 $a(CaPaEBR)ebr10464486 035 $a(OCoLC)714568555 035 $a(DE-B1597)720503 035 $a(DE-B1597)9789027285386 035 $a(EXLCZ)992550000000033080 100 $a20040802d2004 uy 0 101 0 $aeng 135 $aurcn||||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 00$aStudies in Baltic and Indo-European linguistics $ein honor of William R. Schmalstieg /$fedited by Philip Baldi, Pietro U. Dini 205 $a1st ed. 210 $aAmsterdam ;$aPhiladelphia $cJohn Benjamins$dc2004 215 $a1 online resource (xlvi, 302 pages) $cillustrations, map 225 1 $aAmsterdam studies in the theory and history of linguistic science. Series IV, Current issues in linguistic theory,$x0304-0763 ;$vv. 254 300 $aBibliographic Level Mode of Issuance: Monograph 311 0 $a9789027247681 311 0 $a9027247684 311 0 $a9781588115843 311 0 $a1588115844 320 $aIncludes bibliographical references and indexes. 327 $aSTUDIES IN BALTIC AND INDO-EUROPEAN LINGUISTICS -- Editorial page -- Title page -- Copyright page -- Table of contents -- PREFACE AND ACKNOWLEDGMENTS -- WILLIAM R SCHMALSTIEG: THE MAN AND THE SCHOLAR -- PUBLICATIONS 1956-2004 -- ON THE GENITIVE WITH NEUTER PARTICIPLES AND VERBAL NOUNS IN LITHUANIAN -- REFERENCES -- TO BE" OR "NOT TO BE" IN THE INDO-EUROPEAN LANGUAGES -- A verb not for all seasons -- The suppletion strategies -- The irregularity strategies: The zero copula -- A flexible concept (if a concept) as a purely philosophical matter -- The Indo-European case -- REFERENCES -- LITHUANIAN esmì AND esù "I AM" ON THE SPREAD OF THE THEMATIC PRESENT PARADIGMIN INDO-EUROPEAN LANGUAGES -- REFERENCES -- ON THE SUBJECT OF OLD PRUSSIAN ESTATE NAMES -- REFERENCES -- INDO-EUROPEAN *MEN- AND *TBL- -- REFERENCES -- BALTIC PALAEOCOMPARATIVISM AND THE IDEA THAT PRUSSIAN DERIVES FROM GREEK -- Introduction -- Jan Dlugosz and the emergence of a Greek theory of Prussian -- Willichius's best appraisal of the Greek theory of Prussian -- M. Cromer's arguments against D?ugosz's linguistic ideas -- Minor reception of the Greek theory in Western Europe -- Hartknoch and the seventeenth-century reaction against the Greek theory -- A lesser-known case of seventeenth-century reaction: ML Prätorius -- Palaeocomparativistic Prussian-Greek comparisons -- Later echoes of the Greek theory in G, Chr. Pisanski's works -- The Greek theory of Prussian within Baltic palaeocomparativism -- PRIMARY SOURCES -- SECONDARY SOURCES -- PHRASE AND IDIOM IN BRETKE'S OLD LITHUANIAN BIBLE -- A. Old Lithuanian po akim with the possible variant po akiu -- B. On the rendition of Job 16:10 and Exod 15:9 in Luther, Bretke, and the Quandt Bible and elsewhere -- ABBREVIATIONS -- INDO-EUROPEAN *peik- AND BALTIC *peik- -- REFERENCES -- PROCLISIS IN GREEK -- REFERENCES. 327 $aON THE MARKING OF PREDICATE NOMINALS IN BALTIC -- 1. Predicative instrumentais in Baltic -- 2. The expansion of the predicative instrumental as a syntactic default -- 3. Syntactically free uses of the predicative instrumental -- 4. Conclusions -- REFERENCES -- PRUSSICA 1-3 -- 1. A Baltic View of ?niversum -- 2. The possible origin of the OPr. golimban "blue" and the Slavic name of "pigeon -- 3. Old Prussian prassan "millef", Slavic *proso "millet", Tocharian B proks-a "grain -- REFERENCES -- Addendum. On Techarian words for "forest -- FINNISH terve "SOUND, HEALTHY", SLAVONIC *sodorvo "ID.", ANDLITHUANIAN tervétis "RECOVER, MEND, CONVALESCE -- REFERENCES -- DERIVATIONAL MORPHOLOGY OF THE EARLY INDO-EUROPEAN VERB -- 1. Pre-Indo-Eurepean as an active language -- 2. The addition of determinatives to roots in late Pre-Indo-European -- 3. The -k/g- determinative -- 4. The *-t/d- determinative -- 5. The *-s- determinative -- 6. The resonants -- 7. The n-infix -- 8. The*n -infix verbs in Proto-Indo-European and the dialects -- 9. The general pattern of derivational development in Indo-European -- REFERENCES -- IRREGULAR SOUND CHANGE DUE TO FREQUENCY AND THE INTRODUCTION BY SZEMERÉNYI -- REFERENCES -- THOUGHTS ON DECLENSION IN THE OLD PRUSSIAN CATECHISM -- REFERENCES -- PROBLEMS IN THE RECONSTRUCTION OF CERTAIN ENDINGS OF THE LITHUANIAN OPTATIVE -- REFERENCES -- RAIN" AND "ANT" (SUGE E 47 - SAUGIS E 791): HOW ARE THEIR NAMES CONNECTED IN OLD PRUSSIAN? -- LITERATURE AND SOURCES -- HANS M. SCHMIDT-WARTENBERG, A FORGOTTEN BALTICIST -- Additional information -- NEUTER PASSIVE PARTICIPLE IN MODEEN LITHUANIAN -- REFERENCES -- OBSERVATIONS ON THE PARADIGMS OF LITHUANIAN deti "SET, PLACE, LAY" AND dúoti "GIVE -- REFERENCES -- ON THE INDO-EUROPEAN ORIGINS OF GREEK 3RD PL, ACT, IMPERATIVE -v?ov "NEW IMAGE" MORPHOLOGY AND MONOPHTHONGIZATIONS -- REFERENCES. 327 $aOLD PRUSSIAN d?nkauseg?snan -- EEFEEENCES AND ABBREVIATIONS FOR CITED TEXTS -- DOUBLE ORTHOGRAPHY IN AMERICAN LITHUANIAN NEWSPAPERS AT THE TURN OF THE TWENTIETH CENTURY -- 1. Letters ?? ?, ??? -- 2. Theoretical acceptance of ???, ??? in 1898-1899 -- 3. Practical efforts to implement the letters ??? and ??? -- 4. Deviations from the double orthography -- REFERENCES -- HITTITE-za AND REFLEXIVITY MARKING: SOME REMARKS -- REFERENCES -- ONCE MOREABOUT THE "NORTH-RUSSIAN" JINTBA AND ITS MYTHOLOGIZED IMAGE -- REFERENCES -- LATVIAN BRAÑGS: FROM LITHUANIAN, COURONIAN, OE GEEMAN? -- REFERENCES -- THE CELTIC LANGUAGE OF THE IBERIAN PENINSULA -- Study of the Data -- Summary and conclusions -- REFERENCES -- OLD PRUSSIAN" IN M. PRÄTORIUS' DELICIAE PRUSSICAE -- REFERENCES -- NEW DATA ON RESOLVING THE PUZZLE OF THE WOLFENBÜTTEL POSTILLA -- REFERENCES -- INDEX OF AUTHORS -- INDEX OF SUBJECTS -- The series Current Issues in Linguistic Theory. 330 $aThis collection of twenty-nine research papers is dedicated to the eminent Balticist, Slavicist and Indo-Europeanist, William R. Schmalstieg in commemoration of his seventy-fifth birthday. It contains contributions by specialists of mainly Baltic and Indo-European linguistics which are reflective of Schmalstieg's own scholarly interests over the decades of his career, including technical aspects of Baltic and Indo-European phonology, morphology and syntax, etymology, language universals, the history of linguistics and the Baltic text tradition. 410 0$aAmsterdam studies in the theory and history of linguistic science.$nSeries IV,$pCurrent issues in linguistic theory ;$vv. 254. 606 $aBaltic languages 606 $aIndo-European languages 615 0$aBaltic languages. 615 0$aIndo-European languages. 676 $a491/.9 701 $aSchmalstieg$b William R$0565173 701 $aBaldi$b Philip$0311561 701 $aDini$b Pietro U$0220478 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910953334403321 996 $aStudies in Baltic and Indo-European linguistics$94344199 997 $aUNINA LEADER 05152nam 22007815 450 001 9910484821403321 005 20251226202353.0 024 7 $a10.1007/11541868 035 $a(CKB)1000000000213194 035 $a(SSID)ssj0000320356 035 $a(PQKBManifestationID)11274562 035 $a(PQKBTitleCode)TC0000320356 035 $a(PQKBWorkID)10249440 035 $a(PQKB)11067334 035 $a(DE-He213)978-3-540-31820-0 035 $a(MiAaPQ)EBC3067975 035 $a(PPN)123096871 035 $a(EXLCZ)991000000000213194 100 $a20100720d2005 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aTheorem Proving in Higher Order Logics $e18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings /$fedited by Joe Hurd, Tom Melham 205 $a1st ed. 2005. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2005. 215 $a1 online resource (X, 414 p.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v3603 300 $aBibliographic Level Mode of Issuance: Monograph 311 08$a3-540-31820-8 311 08$a3-540-28372-2 320 $aIncludes bibliographical references and index. 327 $aInvited Papers -- On the Correctness of Operating System Kernels -- Alpha-Structural Recursion and Induction -- Regular Papers -- Shallow Lazy Proofs -- Mechanized Metatheory for the Masses: The PoplMark Challenge -- A Structured Set of Higher-Order Problems -- Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS -- Proving Equalities in a Commutative Ring Done Right in Coq -- A HOL Theory of Euclidean Space -- A Design Structure for Higher Order Quotients -- Axiomatic Constructor Classes in Isabelle/HOLCF -- Meta Reasoning in ACL2 -- Reasoning About Java Programs with Aliasing and Frame Conditions -- Real Number Calculations and Theorem Proving -- Verifying a Secure Information Flow Analyzer -- Proving Bounds for Real Linear Programs in Isabelle/HOL -- Essential Incompleteness of Arithmetic Verified by Coq -- Verification of BDD Normalization -- Extensionality in the Calculus of Constructions -- A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic -- A Generic Network on Chip Model -- Formal Verification of a SHA-1 Circuit Core Using ACL2 -- From PSL to LTL: A Formal Validation in HOL -- Proof Pearls -- Proof Pearl: A Formal Proof of Higman?s Lemma in ACL2 -- Proof Pearl: Dijkstra?s Shortest Path Algorithm Verified with ACL2 -- Proof Pearl: Defining Functions over Finite Sets -- Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. 330 $aThis volume constitutes the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), which was held during22?25August2005inOxford,UK.TPHOLscoversallaspectsoftheorem proving in higher order logics as well as related topics in theorem proving and veri?cation. There were 49 papers submitted to TPHOLs 2005 in the full research c- egory, each of which was refereed by at least three reviewers selected by the programcommittee. Of these submissions, 20 researchpapersand 4 proof pearls were accepted for presentation at the conference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2005 also o?ered a venue for the presentation of work in progress, where researchers invited discussion by means of a brief introductory talk and then discussed their work at a poster session. A supplementary proceedings volume was published as a 2005 technical report of the Oxford University Computing Laboratory. The organizers are grateful to Wolfgang Paul and Andrew Pitts for agreeing to give invited talks at TPHOLs 2005. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v3603 606 $aComputer science 606 $aComputer systems 606 $aMachine theory 606 $aSoftware engineering 606 $aArtificial intelligence 606 $aTheory of Computation 606 $aComputer System Implementation 606 $aFormal Languages and Automata Theory 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 606 $aArtificial Intelligence 615 0$aComputer science. 615 0$aComputer systems. 615 0$aMachine theory. 615 0$aSoftware engineering. 615 0$aArtificial intelligence. 615 14$aTheory of Computation. 615 24$aComputer System Implementation. 615 24$aFormal Languages and Automata Theory. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 615 24$aArtificial Intelligence. 676 $a004.0151 701 $aHurd$b Joe$01756654 701 $aMelham$b T. F$g(Tom F.)$01756655 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910484821403321 996 $aTheorem proving in higher order logics$94194083 997 $aUNINA