The Automation of Sound Reasoning and Successful Proof Finding
|Title||The Automation of Sound Reasoning and Successful Proof Finding|
|Publication Type||Book Chapter|
|Year of Publication||2007|
|Authors||Wos, L, Fitelson, B|
|Book Title||Companion to Philosophical Logic|
|Publisher||Blackwell Publishing Ltd.|
The consideration of careful reasoning can be traced to Aristotle and earlier authors. The possibility of rigorous rules for drawing conclusions can certainly be traced to the Middle Ages when types of syllogism were studied. Shortly after the introduction of computers, the audacious scientist naturally envisioned the automation of sound reasoning�reasoning in which conclusions that are drawn follow logically and inevitably from the given hypotheses. Did the idea spring from the intend to emulate Sherlock Holmes and Mr. Spock (of Star Trek) in fiction and Hilbert and Tarski and other great minds in nonfiction? Each of them applied logical reasoning to answer questions, solve problems, and find proofs. But can such logical reasoning be fully automated? Can a single computer program be designed to offer sufficient power in the cited contexts?