Automation of Reasoning: Classical Papers on Computational Logic 1957-1966 by J. SiekmannAutomation of Reasoning: Classical Papers on Computational Logic 1957-1966 by J. Siekmann

Automation of Reasoning: Classical Papers on Computational Logic 1957-1966

byJ. SiekmannEditorG. Wrightson

Paperback | January 10, 2012

Pricing and Purchase Info

$181.71 online 
$219.50 list price save 17%
Earn 909 plum® points

Prices and offers may vary in store

Quantity:

In stock online

Ships free on orders over $25

Not available in stores

about

"Kind of Cl'Ude <_20_c1rl27_27_istmas20_195520_in20_195420_a20_computer20_program20_produced20_what20_appears20_to20_be20_the20_first20_computer20_generated20_mathematical20_proof3a_20_written20_by20_m.20_davis20_at20_the20_institute20_of20_advanced20_studies2c_20_usa2c_20_it20_proved20_a20_number20_theoretic20_theorem20_in20_presburger20_arithmetic.20_christmas20_195520_heralded20_a20_computer20_program20_which20_generated20_the20_first20_proofs20_of20_some20_propositions20_of20_principia20_mathematica2c_20_developed20_by20_a.20_newell2c_20_j.20_shaw2c_20_and20_h.20_simon20_at20_rand20_corporation2c_20_usa.20_in20_sweden2c_20_h.20_prawitz2c_20_d.20_prawitz2c_20_and20_n.20_voghera20_produced20_the20_first20_general20_program20_for20_the20_full20_first20_order20_predicate20_calculus20_to20_prove20_mathematical20_theorems3b_20_their20_computer20_proofs20_were20_obtained20_around20_195720_and20_19582c_20_about20_the20_same20_time20_that20_h.20_gelernter20_finished20_a20_computer20_program20_to20_prove20_simple20_high20_school20_geometry20_theorems.20_since20_the20_field20_of20_computational20_logic20_28_or20_automated20_theorem20_proving29_20_is20_emerging20_from20_the20_ivory20_tower20_of20_academic20_research20_into20_real20_world20_applications2c_20_asserting20_also20_a20_definite20_place20_in20_many20_university20_curricula2c_20_we20_feel20_the20_time20_has20_come20_to20_examine20_and20_evaluate20_its20_history.20_the20_article20_by20_martin20_davis20_in20_the20_first20_of20_this20_series20_of20_volumes20_traces20_the20_most20_influential20_ideas20_back20_to20_the20_27_27_prehistory27_27_20_of20_early20_logical20_thought20_showing20_how20_these20_ideas20_influenced20_the20_underlying20_concepts20_of20_most20_early20_automatic20_theorem20_proving20_programs. _c1rl27_27_istmas="" 1955="" in="" 1954="" a="" computer="" program="" produced="" what="" appears="" to="" be="" the="" first="" generated="" mathematical="" _proof3a_="" written="" by="" m.="" davis="" at="" institute="" of="" advanced="" _studies2c_="" _usa2c_="" it="" proved="" number="" theoretic="" theorem="" presburger="" arithmetic.="" christmas="" heralded="" which="" proofs="" some="" propositions="" principia="" _mathematica2c_="" developed="" a.="" _newell2c_="" j.="" _shaw2c_="" and="" h.="" simon="" rand="" _corporation2c_="" usa.="" _sweden2c_="" _prawitz2c_="" d.="" n.="" voghera="" general="" for="" full="" order="" predicate="" calculus="" prove="" _theorems3b_="" their="" were="" obtained="" around="" 1957="" _19582c_="" about="" same="" time="" that="" gelernter="" finished="" simple="" high="" school="" geometry="" theorems.="" since="" field="" computational="" logic="" _28_or="" automated="" _proving29_="" is="" emerging="" from="" ivory="" tower="" academic="" research="" into="" real="" world="" _applications2c_="" asserting="" also="" definite="" place="" many="" university="" _curricula2c_="" we="" feel="" has="" come="" examine="" evaluate="" its="" history.="" article="" martin="" this="" series="" volumes="" traces="" most="" influential="" ideas="" back="" _27_27_prehistory27_27_="" early="" logical="" thought="" showing="" how="" these="" influenced="" underlying="" concepts="" automatic="" proving="">
Title:Automation of Reasoning: Classical Papers on Computational Logic 1957-1966Format:PaperbackDimensions:528 pagesPublished:January 10, 2012Publisher:Springer-Verlag/Sci-Tech/TradeLanguage:English

The following ISBNs are associated with this title:

ISBN - 10:3642819540

ISBN - 13:9783642819544

Look for similar items by category:

Reviews

Table of Contents

The Prehistory and Early History of Automated Deduction.- Mechanical Proof Search and the Theory of Logical Deduction in the USSR.- 1957.- A Computer Program for Presburger's Algorithm.- Empirical Explorations with the Logic Theory Machine: A Case Study in Heuristics.- Proving a Theorem (as Done by Man, Logician or Machine).- 1958.- On Machines Which Prove Theorems.- 1959.- A non-heuristic Program for Proving Elementary Logical Theorems.- Realization of a Geometry-Theorem Proving Machine.- 1960.- A Computing Procedure for Quantification Theory.- Empirical Explorations of the Geometry-Theorem Proving Machine.- A Proof Method for Quantification Theory: Its Justification and Realization.- An Improved Proof Procedure.- A Mechanical Proof Procedure and its Realization in an Electronic Computer.- Proving Theorems by Pattern Recognition.- Toward Mechical Mathematics.- 1962.- A Machine Program for Theorem Proving.- Theorem Testing by Computer.- Exploratory Mathematics by Machine.- Machine-Generated Problem-Solving Graphs.- 1963.- Eliminating the Irrelevant from Mechanical Proofs.- A Semi-Decision Procedure for the Functional Calculus.- A Computer Program for a Solvable Case of the Decision Problem.- A Simplified Proof Method for Elementary Logic.- Theorem-Proving on the Computer.- 1964.- The Unit Preference Strategy in Theorem Proving.- 1965.- A Machine Oriented Logic Based on the Resolution Principle.- Automatic Deduction with Hyper-Resolution.- An Algorithm for a Machine Search of a Natural Logical Deduction in a Propositional Calculus.- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving.- 1966.- Theorem-Proving for Computers: Some Results on Resolution and Renaming.- Bibliography on Computational Logic.