LEADER 06873nam 22005295 450 001 996465689403316 005 20200706094648.0 010 $a3-540-39216-5 024 7 $a10.1007/BFb0012819 035 $a(CKB)1000000000230756 035 $a(SSID)ssj0000320754 035 $a(PQKBManifestationID)11283767 035 $a(PQKBTitleCode)TC0000320754 035 $a(PQKBWorkID)10258581 035 $a(PQKB)11454969 035 $a(DE-He213)978-3-540-39216-3 035 $a(PPN)155215248 035 $a(EXLCZ)991000000000230756 100 $a20121227d1988 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$a9th International Conference on Automated Deduction$b[electronic resource] $eArgonne, Illinois, USA, May 23-26, 1988. Proceedings /$fedited by Ewing Lusk, Ross Overbeek 205 $a1st ed. 1988. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1988. 215 $a1 online resource (X, 776 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v310 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-19343-X 327 $aFirst-order theorem proving using conditional rewrite rules -- Elements of Z-module reasoning -- Learning and applying generalised solutions using higher order resolution -- Specifying theorem provers in a higher-order logic programming language -- Query processing in quantitative logic programming -- An environment for automated reasoning about partial functions -- The use of explicit plans to guide inductive proofs -- Logicalc: An environment for interactive proof development -- Implementing verification strategies in the KIV-system -- Checking natural language proofs -- Consistency of rule-based expert systems -- A mechanizable induction principle for equational specifications -- Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time -- Towards efficient "knowledge-based" automated theorem proving for non-standard logics -- Propositional temporal interval logic is PSPACE complete -- Computational metatheory in Nuprl -- Type inference in Prolog -- Procedural interpretation of non-horn logic programs -- Recursive query answering with non-horn clauses -- Case inference in resolution-based languages -- Notes on Prolog program transformations, Prolog style, and efficient compilation to the Warren abstract machine -- Exploitation of parallelism in prototypical deduction problems -- A decision procedure for unquantified formulas of graph theory -- Adventures in associative-commutative unification (A summary) -- Unification in finite algebras is unitary(?) -- Unification in a combination of arbitrary disjoint equational theories -- Partial unification for graph based equational reasoning -- SATCHMO: A theorem prover implemented in Prolog -- Term rewriting: Some experimental results -- Analogical reasoning and proof discovery -- Hyper-chaining and knowledge-based theorem proving -- Linear modal deductions -- A resolution calculus for modal logics -- Solving disequations in equational theories -- On word problems in Horn theories -- Canonical conditional rewrite systems -- Program synthesis by completion with dependent subtypes -- Reasoning about systems of linear inequalities -- A subsumption algorithm based on characteristic matrices -- A restriction of factoring in binary resolution -- Supposition-based logic for automated nonmonotonic reasoning -- Argument-bounded algorithms as a basis for automated termination proofs -- Two automated methods in implementation proofs -- A new approach to universal unfication and its application to AC-unification -- An implementation of a dissolution-based system employing theory links -- Decision procedure for autoepistemic logic -- Logical matrix generation and testing -- Optimal time bounds for parallel term matching -- Challenge equality problems in lattice theory -- Single axioms in the implicational propositional calculus -- Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programs -- Challenge problems from nonassociative rings for theorem provers -- An interactive enhancement to the Boyer-Moore theorem prover -- A goal directed theorem prover -- m-NEVER system summary -- EFS ? An interactive Environment for Formal Systems -- Ontic: A knowledge representation system for mathematics -- Some tools for an inference laboratory (ATINF) -- Quantlog: A system for approximate reasoning in inconsistent formal systems -- LP: The larch prover -- The KLAUS automated deduction system -- A Prolog technology theorem prover -- ?Prolog: An extended logic programming language -- SYMEVAL: A theorem prover based on the experimental logic -- ZPLAN: An automatic reasoning system for situations -- The TPS theorem proving system -- MOLOG: A modal PROLOG -- PARTHENON: A parallel theorem prover for non-horn clauses -- An nH-Prolog implementation -- RRL: A rewrite rule laboratory -- Geometer: A theorem prover for algebraic geometry -- Isabelle: The next seven hundred theorem provers -- The CHIP system : Constraint handling in Prolog. 330 $aThis volume contains the papers presented at the Ninth International Conference on Automated Deduction (CADE-9) held May 23-26 at Argonne National Laboratory, Argonne, Illinois. The conference commemorates the twenty-fifth anniversary of the discovery of the resolution principle, which took place during the summer of 1963. The CADE conferences are a forum for reporting on research on all aspects of automated deduction, including theorem proving, logic programming, unification, deductive databases, term rewriting, ATP for non-standard logics, and program verification. All papers submitted to the conference were refereed by at least two referees, and the program committee accepted the 52 that appear here. Also included in this volume are abstracts of 21 implementations of automated deduction systems. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v310 606 $aMathematical logic 606 $aMathematical Logic and Foundations$3https://scigraph.springernature.com/ontologies/product-market-codes/M24005 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 615 0$aMathematical logic. 615 14$aMathematical Logic and Foundations. 615 24$aMathematical Logic and Formal Languages. 676 $a511.3 702 $aLusk$b Ewing$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aOverbeek$b Ross$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a996465689403316 996 $a9th International Conference on Automated Deduction$92831318 997 $aUNISA LEADER 02038oam 2200505 450 001 9910709637603321 005 20180607095003.0 035 $a(CKB)5470000002471862 035 $a(OCoLC)896811054 035 $a(OCoLC)995470000002471862 035 $a(EXLCZ)995470000002471862 100 $a20141123d1983 ua 0 101 0 $aeng 135 $aurmn||||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aApplication of total-count aeroradiometric maps to the exploration for heavy-mineral deposits in the coastal plain of Virginia /$fby Andrew E. Grosz; with a section on Field-spectrometer-data reduction by Kenneth L. Kosanke 210 1$aWashington :$cUnited States Department of the Interior, Geological Survey,$d1983. 215 $a1 online resource (iii, 20 pages) $cillustrations, map +$e5 plates 225 1 $aGeological Survey professional paper ;$v1263 300 $a"A method of exploration for nearshore marine placer heavy-mineral deposits by the use of gamma-ray ground-radiometric and aeroradiometric techniques." 320 $aIncludes bibliographical references (pages 18-20). 517 1 $aAeroradiometric maps, exploration for heavy-mineral deposits 606 $aHeavy minerals$zVirginia 606 $aRadioactive prospecting$zVirginia 606 $aHeavy minerals$2fast 606 $aRadioactive prospecting$2fast 607 $aVirginia$2fast 615 0$aHeavy minerals 615 0$aRadioactive prospecting 615 7$aHeavy minerals. 615 7$aRadioactive prospecting. 700 $aGrosz$b A. E$g(Andrew E.),$01414569 702 $aKosanke$b Kenneth L. 712 02$aGeological Survey (U.S.), 801 0$bCOP 801 1$bCOP 801 2$bOCLCO 801 2$bOCLCF 801 2$bGPO 906 $aBOOK 912 $a9910709637603321 996 $aApplication of total-count aeroradiometric maps to the exploration for heavy-mineral deposits in the coastal plain of Virginia$93542959 997 $aUNINA LEADER 02347nam 2200553 a 450 001 9910791048003321 005 20161219111706.0 010 $a1-5443-5027-9 010 $a1-4833-4936-5 010 $a1-4833-0120-6 035 $a(CKB)2550000001273223 035 $a(CaPaEBR)ebrary10863094 035 $a(SSID)ssj0001184658 035 $a(PQKBManifestationID)12512344 035 $a(PQKBTitleCode)TC0001184658 035 $a(PQKBWorkID)11195799 035 $a(PQKB)11194061 035 $a(MiAaPQ)EBC1675580 035 $a(OCoLC)877868592 035 $a(StDuBDS)EDZ0000174437 035 $a(EXLCZ)992550000001273223 100 $a20131121d2013 fy 0 101 0 $aeng 135 $aur||||||||||| 181 $ctxt 182 $cc 183 $acr 200 00$aInterest groups unleashed$b[electronic resource] /$feditors, Paul S. Herrnson, Christopher J. Deering, Clyde Wilcox 210 $aThousand Oaks, Calif. $cCQ Press$d2013 215 $a1 online resource (xiii, 285 p.) $cill 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a1-4522-0378-4 311 $a1-306-64013-X 320 $aIncludes bibliographical references and index. 330 8 $aThe 2010 US campaign and election was pivotal: the Republican takeover of the House, the advent of 'super PACs', and record-breaking sums spent on a midterm election. More than ever before, interest groups were able to mobilise new resources and new technologies in a shifting set of House and Senate races. This volume explores - in a series of lively case studies - a cross-section of groups, communities, and networks that vividly illustrates the 'unleashing' of interest group activity in the electoral process in response to Citizens United and other court cases and events. 606 $aPressure groups$zUnited States$xHistory$y21st century 606 $aElections$zUnited States$xHistory$y21st century 615 0$aPressure groups$xHistory 615 0$aElections$xHistory 676 $a322.430973 701 $aHerrnson$b Paul S.$f1958-$0884569 701 $aDeering$b Christopher J.$f1951-$01547921 701 $aWilcox$b Clyde$f1953-$01084244 801 0$bStDuBDS 801 1$bStDuBDS 906 $aBOOK 912 $a9910791048003321 996 $aInterest groups unleashed$93804536 997 $aUNINA