Missing Proofs Found
Tóm tắt
For close to a century, despite the efforts of fine minds that include Hilbert and Ackermann, Tarski and Bernays, Łukasiewicz, and Rose and Rosser, various proofs of a number of significant theorems have remained missing – at least not reported in the literature – amply demonstrating the depth of the corresponding problems. The types of such missing proofs are indeed diverse. For one example, a result may be guaranteed provable because of being valid, and yet no proof has been found. For a second example, a theorem may have been proved via metaargument, but the desired axiomatic proof based solely on the use of a given inference rule may have eluded the experts. For a third example, a theorem may have been announced by a master, but no proof was supplied. The finding of missing proofs of the cited types, as well as of other types, is the focus of this article. The means to finding such proofs rests with heavy use of McCune's automated reasoning program OTTER, reliance on a variety of powerful strategies this program offers, and employment of diverse methodologies. Here we present some of our successes and, because it may prove useful for circuit design and program synthesis as well as in the context of mathematics and logic, detail our approach to finding missing proofs. Well-defined and unmet challenges are included.
Tài liệu tham khảo
Epstein, R.: The Semantic Foundations of Logic: Propositional Logics, 2nd edn, Oxford University Press, New York, 1994.
Harris, K. and Fitelson, B.: Distributivity in Łℵ0 and other sentential logics, J. Automated Reasoning (2001), this issue.
Hilbert, D. and Ackermann, W.: Principles of Mathematical Logic, Chelsea, New York, 1950.
Łukasiewicz, J.: Elements of Mathematical Logic, Macmillan, New York, 1963.
Łukasiewicz, J.: Selected Works, edited by L. Borokowski, North-Holland, Amsterdam, 1970.
McCune, W.: OTTER 3.0 reference manual and guide, Tech. Report ANL-94/6, Argonne National Laboratory, Argonne, IL, 1994.
McCune, W.: Solution of the Robbins problem, J. Automated Reasoning 19(3) (1997), 263-276.
McCune, W. and Shumsky, O.: IVY: A preprocessor and proof checker for first-order logic, in M. Kaufmann, P. Manolios, and J. Moore (eds.), Computer-Aided Reasoning: ACL2 Case Studies, Chapter 16, Kluwer Academic Publishers, Dordrecht, 2000.
Meredith, C. A.: Single axioms for the systems (C, N), (C, 0), and (A, N) of the two-valued propositional calculus, J. Computing Systems 1(3) (1953), 155-164.
Meredith, C. A.: The dependence of an axiom of Łukasiewicz, Trans. Amer. Math. Soc. 87(1) (1958), 54.
Meredith, C. A. and Prior, A.: Notes on the axiomatics of the propositional calculus, Notre Dame J. Formal Logic 4(3) (1963), 171-187.
Prior, A.: Formal Logic, Clarendon Press, Oxford, 1960.
Rose, A. and Rosser, J. B.: Fragments of many-valued statement calculi, Trans. Amer. Math. Soc. 87 (1958), 1-53.
Ulrich, D.: A legacy recalled and a tradition continued, J. Automated Reasoning (2001), this issue.
Veroff, R.: Solving open questions and other challenge problems using proof sketches, J. Automated Reasoning (2001), this issue.
Wajsberg, M.: Logical Works, Polish Academy of Sciences, Warsaw, 1977.
Wos, L., Robinson, G., and Carson, D.: Efficiency and completeness of the set of support strategy in theorem proving, J. Assoc. Comput. Mach. 12(4) (1965), 536-541.
Wos, L., Robinson, G., Carson, D., and Shalla, L.: The concept of demodulation in theorem proving, J. Assoc. Comput. Mach. 14(4) (October 1967), 698-709.
Wos, L.: The resonance strategy, Comput. Math. Appl. 29(2) (February 1995), 133-178.
Wos, L.: OTTER and theMoufang identity problem, J. Automated Reasoning 17(2) (1996), 215-257.
Wos, L. and Pieper, G. W.: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning, World Scientific, Singapore, 1999a.
Wos, L. and Pieper, G. W.: The hot list strategy, J. Automated Reasoning 22(1) (1999b), 1-44.
Wos, L. and Pieper, G. W.: The Collected Works of Larry Wos, World Scientific, 2000.
Wos, L.: Conquering the Meredith single axiom, J. Automated Reasoning (2001), this issue.