Conquering the Meredith Single Axiom
|Title||Conquering the Meredith Single Axiom|
|Year of Publication||2000|
|Series Title||J. Automated Reasoning|
For more than three and one-half decades beginning in the early 1960s, a heavy emphasis on proof finding has been a key component of the Aargonne paradigm, whose use has directly led to significant advances in automated reasoning and important contributions to mathematics and logic. The theorems that have served well range from the trivial to the deep, even including some that corresponded to open questions. Often the paradigm asks for a theorem whose proof is in hand but that cannot be obtained in a fully automated manner by the program in use. The theoirem whose hypothesis consists solely of the Meredith single axiom for two-valued sentential (or propositional) calculus and whose conclusion is the Lukasiewicz three-axiom system for that area of formal logic was just such a theorem. Featured in this article is the methodology that enabled the program OTTER to find the first fully autoamted proof of the cited theorem, a proof with the intriguing property that none of its steps contains a term of the form n(n(t)) for any term t. As evidence of the power of the new methodology, the article also discusses OTTER\'s success in obtaining the first known rpoof of a theorem concerning a single axiom of Lukasiewicz.