The Automation of Sound Reasoning and Successful Proof Finding

TitleThe Automation of Sound Reasoning and Successful Proof Finding
Publication TypeBook Chapter
Year of Publication2007
AuthorsWos, L, Fitelson, B
Book TitleCompanion to Philosophical Logic
PublisherBlackwell Publishing Ltd.
CityOxford, UK
Other NumbersANL/MCS-P811-0500

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?