LEADER 06345nam 22005535 450 001 996465940003316 005 20200630174056.0 010 $a3-540-39861-9 024 7 $a10.1007/3-540-16780-3 035 $a(CKB)1000000000230543 035 $a(SSID)ssj0000320753 035 $a(PQKBManifestationID)11264086 035 $a(PQKBTitleCode)TC0000320753 035 $a(PQKBWorkID)10259111 035 $a(PQKB)11582402 035 $a(DE-He213)978-3-540-39861-5 035 $a(PPN)155210688 035 $a(EXLCZ)991000000000230543 100 $a20121227d1986 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$a8th International Conference on Automated Deduction$b[electronic resource] $eOxford, England, July 27- August 1, 1986. Proceedings /$fedited by Jörg H. Siekmann 205 $a1st ed. 1986. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1986. 215 $a1 online resource (XII, 716 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v230 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-16780-3 327 $aConnections and higher-order logic -- Commutation, transformation, and termination -- Full-commutation and fair-termination in equational (and combined) term-rewriting systems -- An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations -- Proving termination of associative commutative rewriting systems by rewriting -- Relating resolution and algebraic completion for Horn logic -- A simple non-termination test for the Knuth-Bendix method -- A new formula for the execution of categorical combinators -- Proof by induction using test sets -- How to prove equivalence of term rewriting systems without induction -- Sufficient completeness, term rewriting systems and ?anti-unification? -- A new method for establishing refutational completeness in theorem proving -- A theory of diagnosis from first principles -- Some contributions to the logical analysis of circumscription -- Modal theorem proving -- Computational aspects of three-valued logic -- Resolution and quantified epistemic logics -- A commonsense theory of nonmonotonic reasoning -- Negative paramodulation -- The heuristics and experimental results of a new hyperparamodulation: HL-resolution -- ECR: An equality conditional resolution proof procedure -- Using narrowing to do isolation in symbolic equation solving ? an experiment in automated reasoning -- Formulation of induction formulas in verification of prolog programs -- Program verifier "Tatzelwurm": Reasoning about systems systems of linear inequalities -- An interactive verification system based on dynamic logic -- What you always wanted to know about clause graph resolution -- Parallel theorem proving with connection graphs -- Theory links in semantic graphs -- Abstraction using generalization functions -- An improvement of deduction plans: Refutation plans -- Controlling deduction with proof condensation and heuristics -- Nested resolution -- Mechanizing constructive proofs -- Implementing number theory: An experiment with Nuprl -- Parallel algorithms for term matching -- Unification in combinations of collapse-free theories with disjoint sets of function symbols -- Combination of unification algorithms -- Unification in the data structure sets -- NP-completeness of the set unification and matching problems -- Matching with distributivity -- Unification in boolean rings -- Some relationships between unification, restricted unification, and matching -- A classification of many-sorted unification problems -- Unification in many-sorted equational theories -- Classes of first order formulas under various satisfiability definitions -- Diamond formulas in the dynamic logic of recursively enumerable programs -- A prolog machine -- A prolog technology theorem prover: Implementation by an extended prolog compiler -- Paths to high-performance automated theorem proving -- Purely functional implementation of a logic -- Causes for events: Their computation and applications -- How to clear a block: Plan formation in situational logic -- Deductive synthesis of sorting programs -- The TPS theorem proving system -- Trspec: A term rewriting based system for algebraic specifications -- Highly parallel inference machine -- Automatic theorem proving in the ISDV system -- The karlsruhe induction theorem proving system -- Overview of a theorem-prover for a computational logic -- GEO-prover ? A geometry theorem prover developed at UT -- The markgraf karl refutation procedure (MKRP) -- The J-machine: Functional programming with combinators -- The illinois prover: A general purpose resolution theorem prover -- Theorem proving systems of the Formel project -- The passau RAP system: Prototyping algebraic specifications using conditional narrowing -- RRL: A rewrite rule laboratory -- A geometry theorem prover based on Buchberger's algorithm -- REVE a rewrite rule laboratory -- ITP at argonne national laboratory -- Autologic at university of victoria -- Thinker -- The KLAUS automated deduction system -- The KRIPKE automated theorem proving system -- SHD-prover at university of texas at austin. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v230 606 $aMathematical logic 606 $aArtificial intelligence 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 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 615 0$aMathematical logic. 615 0$aArtificial intelligence. 615 14$aMathematical Logic and Foundations. 615 24$aMathematical Logic and Formal Languages. 615 24$aArtificial Intelligence. 676 $a511.3 702 $aSiekmann$b Jörg H$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a996465940003316 996 $a8th International Conference on Automated Deduction$92831112 997 $aUNISA LEADER 05784nam 2200733 a 450 001 9910960965003321 005 20251116140423.0 010 $a9786610203253 010 $a9781280203251 010 $a1280203250 010 $a9780309565844 010 $a0309565847 010 $a9780585085555 010 $a0585085552 035 $a(CKB)110986584751182 035 $a(EBL)3376492 035 $a(SSID)ssj0000236386 035 $a(PQKBManifestationID)11216529 035 $a(PQKBTitleCode)TC0000236386 035 $a(PQKBWorkID)10172876 035 $a(PQKB)11627219 035 $a(Au-PeEL)EBL3376492 035 $a(CaPaEBR)ebr10056765 035 $a(OCoLC)940510235 035 $a(MiAaPQ)EBC3376492 035 $a(Perlego)4735827 035 $a(BIP)1364157 035 $a(EXLCZ)99110986584751182 100 $a19920423d1992 uy 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aResearch and education reform $eroles for the Office of Educational Research and Improvement /$fRichard C. Atkinson and Gregg B. Jackson, editors 205 $a1st ed. 210 $aWashington, D.C. $cNational Academy Press$d1992 215 $a1 online resource (203 pages) 300 $a"Committee on the Federal Role in Education Research, Commission on Behavioral and Social Sciences and Education, National Research Council." 311 0 $a9780309047296 311 0 $a0309047293 320 $aIncludes bibliographical references (p. 173-187). 327 $aResearch and Education Reform; Copyright; Contents; Preface; Executive Summary; CONCLUSIONS; RECOMMENDATIONS; Mission, Governance, and Agenda; Organization and Functions; Operations; Funding; 1 Introduction; THE CHALLENGE OF EDUCATION REFORM; THE ROLE OF RESEARCH; 2 Research and the Improvement of Education; BASIC RESEARCH IN COGNITIVE SCIENCE; Mathematics Education; Reading; CURRICULUM DEVELOPMENT AND IMPROVED TEACHING APPROACHES; Project IMPACT; Program Description; Testing and Evaluation; Reading Recovery; Program Description; Research and Development; Testing and Evaluation 327 $aReciprocal Teaching; Program Description; Testing and Evaluation; The Comprehensive School Mathematics Program; Program Description; Research and Development; Testing and Evaluation; Cognitively Guided Instruction; Research Description; Testing and Evaluation; Computer-Assisted Instruction; Program Description; Testing and Evaluation; Cooperative Learning; Program Description; Research and Development; Testing and Evaluation; SCHOOL RESTRUCTURING; School Development Program; Program Description; Testing and Evaluation; Outcomes Driven Development Model; Program Description 327 $aTesting and Evaluation; MONITORING THE STATE OF PUBLIC EDUCATION; National Statistics; Longitudinal Studies; National Assessment of Educational Progress; International Studies; CONGRESSIONAL USE OF EDUCATION RESEARCH; CONCLUSIONS; 3 The Office of Educational Research and Improvement; HISTORY; Centers, Laboratories, and the Educational Resources Information Center; The National Institute of Education; The Office of Educational Research and Improvement; ORGANIZATION AND ACTIVITIES; The National Advisory Council on Educational Research and Improvement; Office of the Assistant Secretary 327 $aOffice of Research; National R&D Centers; Field-Initiated Research; Educational Resources Information Center; Programs for the Improvement of Practice; Regional Laboratories; Program Effectiveness Panel and National Diffusion Network; Fund for the Improvement and Reform of Schools and Teaching; National Center for Educational Statistics; Library Programs; OPERATIONS AND FUNDING; Staffing; Procurement; Funding of the Centers and Laboratories; Peer Review; Report Review and Clearance Procedures; Funding; OERI's 1991 Budget; Comparisons with Other Fields; Other Funding of R&D; 4 Appraisal of OERI 327 $aMISSION AND OBJECTIVES; Mission; Continuing Controversy About Education; A History of ""Politicization""; GOVERNANCE; FUNDING; COORDINATION AND COOPERATION; SUSTAINED EFFORTS; QUALITY ASSURANCE AND ACCUMULATION OF RESULTS; LINKAGES WITH PRACTICE; 5 Recommendations; MISSION, GOVERNANCE, AND AGENDA; ORGANIZATION AND FUNCTIONS; OPERATIONS; FUNDING; CONCLUSION; References; Appendix Biographical Sketches of Committee Members and Staff 330 $aThe Office of Educational Research and Improvement (OERI) in the U.S. Department of Education has a mandate for expanding knowledge of teaching and learning and for improving education in this country. This book focuses on how OERI can better fulfill that mission in light of what is known about why prior education reforms have often failed, what is needed to enhance the effectiveness of such efforts, and what education research and development can contribute to better schools. The history, mission, governance, organization, functions, operations, and budgets of OERI are analyzed. Recommendations are made for restructuring OERI, expanding funding, involving scholars from many fields, and engaging teachers and school principals in improvement efforts. 606 $aEducation$xResearch$zUnited States 606 $aEducational innovations$zUnited States 606 $aEducational change$zUnited States 615 0$aEducation$xResearch 615 0$aEducational innovations 615 0$aEducational change 676 $a370/.78073 701 $aAtkinson$b Richard C$050808 701 $aJackson$b Gregg B$01814283 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910960965003321 996 $aResearch and education reform$94368028 997 $aUNINA