World Scientific
  • Search
Skip main navigation

Cookies Notification

We use cookies on this site to enhance your user experience. By continuing to browse the site, you consent to the use of our cookies. Learn More
×
Our website is made possible by displaying certain online content using javascript.
In order to view the full content, please disable your ad blocker or whitelist our website www.worldscientific.com.

System Upgrade on Tue, Oct 25th, 2022 at 2am (EDT)

Existing users will be able to log into the site and access content. However, E-commerce and registration of new users may not be available for up to 12 hours.
For online purchase, please visit us again. Contact us at [email protected] for any enquiries.

Shortening of Proof Length is Elusive for Theorem Provers

    There are many examples of failed strategies whose intention is to optimize a process but instead they produce worse results than no strategy at all. Many fall under the loose umbrella of the “no free lunch theorem”. In this paper we present an example in which a simple (but assumedly naive) strategy intended to shorten proof lengths in the propositional calculus produces results that are significantly worse than those achieved without any method to try to shorten proofs.This contrast with what was to be expected intuitively, namely no improvement in the length of the proofs. Another surprising result is how early the naive strategy failed. We set up a experiment in which we sample random classical propositional theorems and then feed them to two very popular automatic theorem provers (AProS and Prover9). We then compared the length of the proofs obtained under two methods: (1) the application of the theorem provers with no additional information; (2) the addition of new (redundant) axioms to the provers. The second method produced even longer proofs than the first one.

    References