David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Most automated theorem provers are clausal-form provers based on variants of resolutionrefutation. In my , I described the theorem prover OSCAR that was based instead on natural deduction. Some limited evidence was given suggesting that OSCAR was suprisingly efficient. The evidence consisted of a handful of problems for which published data was available describing the performance of other theorem provers. This evidence was suggestive, but based upon too meager a comparison to be conclusive. The question remained, “How does natural deduction compare with resolution-refutation?” In the ensuing seven years, OSCAR has evolved in important ways, and other developments have made it possible to collect more accurate comparative data. Specifically, the creation of the TPTP library of problems for theorem provers,1 and the availability of important theorem provers on the world wide web, make objective comparisons easier. These developments recently inspired Geoff Sutcliffe, one of the founders of the TPTP library, to issue a challenge to OSCAR. At CADE-13, a competition was held for clausal-form theorem provers.2 Otter was one of the most successful contestants. In addition, Otter is able to handle problems stated in natural form (as opposed to clausal form), and Otter is readily available for different platforms.3 Sutcliffe selected 212 problems from the TPTP library, and suggested that OSCAR and Otter run these problems on the same hardware. This “Shootout at the ATP corral” took place, with the result that OSCAR was on the average 40 times faster than Otter. In addition, OSCAR was able to find proofs for 16 problems on which Otter failed, and Otter was able to find proofs for 3 problems on which OSCAR failed. Taking into account that Otter was written in C and OSCAR in LISP, the speed difference of the algorithms themselves could be as much as an order of magnitude greater. Apparently, natural deduction has some advantages over resolution-refutation..
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Hartley Slater (2008). Harmonising Natural Deduction. Synthese 163 (2):187 - 198.
Francis Jeffry Pelletier (1998). Automated Natural Deduction in Thinker. Studia Logica 60 (1):3-43.
Leopold Stubenberg (1992). What is It Like to Be Oscar? Synthese 90 (1):1-26.
Added to index2009-01-28
Total downloads18 ( #150,601 of 1,725,090 )
Recent downloads (6 months)9 ( #72,301 of 1,725,090 )
How can I increase my downloads?