Octopus: combining learning and parallel search. (English) Zbl 1102.68647

Summary: This paper presents Octopus, an automated theorem-proving system that combines learning and parallel search. The learning technique involves proving a simpler version of a given theorem and then using what it has learned to prove the given theorem. As of January 2004 Octopus had successfully proved 43 of the 1.0-rated theorems of the TPTP Problem Library.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI


[1] Newborn, M.: Automated Theorem Proving: Theory and Practice, Springer-Verlag, New York, 2001. · Zbl 0963.68176
[2] Sutcliffe, G. and Suttner, C. B.: The TPTP problem library, J. Automated Reasoning 21(2) (1998), 177-203. · Zbl 0910.68197
[3] http://www.cs.miami.edu/\(\sim\)tptp/
[4] http://www.cs.miami.edu/\(\sim\)tptp/CASC/
[5] Newborn, M.: Proofs of twenty-four 1.0-rated theorems in the TPTP problem library, TR SOCS-03.6, School of Computer Science, McGill University, Montreal, 2003.
[6] Newborn, M. and Wang, Z.: Proofs of nineteen more 1.0 rated theorems in the TPTP problem library, TR SOCS-04.1, School of Computer Science, McGill University, Montreal, 2004.
[7] Plaisted, D. A.: Theorem proving with abstraction, Artificial Intelligence 16(1) (1981), 47-108. · Zbl 0454.68113
[8] Kling, R. E.: A paradigm for reasoning by analogy, Artificial Intelligence 2(2) (1971), 147-178. · Zbl 0227.68041
[9] Greiner, R.: Learning and understanding by analogies, Artificial Intelligence 35(1) (1988), 81-125. · Zbl 0646.68095
[10] Brock, B., Cooper, S. and Pierce, W.: Analogical reasoning and proof discovery, in E. Lusk and R. A. Overbeek (eds.), Proc. 9th Conf. on Automated Deduction, Argonne, IL, LNCS 310, Springer-Verlag, 1988, pp. 454-468. · Zbl 0666.68096
[11] Carbonell, J. G. and Veloso, M.: Integrating derivational analogy into a general problem solving architecture, in J. Kolodner (ed.), Proc. 1988 DARPA Workshop on Case-Based Reasoning, Clearwater Beach, 1988.
[12] Kolbe, T. and Brauburger, J.: Plagiator ? a learning prover, in W. McCune (ed.), Proc. 14th Int. Conf. on Automated Deduction, LNCS 1249, Springer-Verlag, 1997, pp. 256-259.
[13] Kolbe, T. and Walther, C.: Reusing proofs, in A. G. Cohn (ed.), Proc. 11th European Conf. on Artificial Intelligence, Amsterdam, Wiley, 1994, pp. 80-84.
[14] Melis, E.: A model of analogy-driven proof-plan construction, in C. S. Mellish (ed.), Proc. 14th Int. Joint Conf. on Artificial Intelligence, Morgan Kaufmann, 1995, pp. 182-189.
[15] Draeger, J.: Acquisition of useful lemma knowledge in automated reasoning, in F. Giunchiglia (ed.), Proc. 8th Int. Conf. on Artificial Intelligence: Methodology, Systems, and Applications, LNCS 1480, Springer-Verlag, 1998, pp. 230-239.
[16] Fuchs, M.: Experiments in the heuristic use of past proof experience, in M. A. McRobbie and J. K. Slaney (eds.), Proc. 13th Conf. on Automated Deduction, LNAI 1104, Springer-Verlag, 1996, pp. 523-537.
[17] Denzinger, J. and Schulz, S.: Learning domain knowledge to improve theorem proving, in M. A. McRobbie and J. K. Slaney (eds.), Proc. 13th Conf. on Automated Deduction, LNAI 1104, Springer-Verlag, 1996, pp. 62-76.
[18] Denzinger, J., Fuchs, M., Goller, C. and Schulz, S.: Learning from previous proof experience: A survey, Report AR-99-4, Fakultät für Informatik der Technischen Universität München, 1999.
[19] Bonacina, M. P.: A taxonomy of parallel strategies for deduction, Ann. Math. Artificial Intelligence 29(1-4) (2000), 223-257. · Zbl 1001.68124
[20] Jindal, A., Overbeek, R. and Kabat, W.: Exploitation of parallel processing for implementing high-performance deduction systems, J. Automated Reasoning 8(1) (1992), 23-38.
[21] Lusk, E. L. and McCune, W. W.: Experiments with ROO: A parallel automated deduction system, in B. Fronhofer and G. Wrightson (eds.), Parallelization in Inference Systems, LNAI 590, Springer-Verlag, 1990, pp. 139-162.
[22] Lusk, E., McCune, W. and Slaney, J.: ROO ? a parallel theorem prover, ANL/MCS-TM-149, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, 1991.
[23] Lusk, E. L., McCune, W. W. and Slaney, J. K.: ROO: A parallel theorem prover, in D. Kapur (ed.), Proc. 11th Int. Conf. on Automated Deduction, Saratoga Springs, June 15-18, LNAI 607, Springer-Verlag, 1992, pp. 731-734.
[24] Bonacina, M. P. and Hsiang, J.: Distributed deduction by clause-diffusion: Distributed contraction and the Aquarius prover, J. Symbolic Computation 19(3) (1995), 245-267. · Zbl 0836.68105
[25] Bonacina, M. P.: Combination of distributed search and multi-search in Peers-mcd.d, in R. Gore, A. Leitsch and T. Nipkow (eds.), Proc. 1st Int. Joint Conf. on Automated Reasoning, Siena, Italy, June 18-23, LNAI 2083, Springer-Verlag, 2001, pp. 448-452. · Zbl 0988.68611
[26] Bonacina, M. P.: The clause-diffusion theorem prover Peers-mcd (system description), in W. McCune (ed.), Proc. 14th Int. Conf. on Automated Deduction, Townsville, Australia, July 13-17, LNCS 1249, Springer-Verlag, 1997, pp. 53-56.
[27] McCune, W.: Otter 3.3 reference manual, Technical Memorandum No. 263, Mathematics and Computer Science Division, Argonne National Laboratory, 2003 (http://www-unix.mcs.anl.gov/AR/otter/otter33.pdf).
[28] McCune, W.: 33 basic test problems: A practical evaluation of some paramodulation strategies, in R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1997.
[29] Letz, R., Bayerl, S., Schumann, J. and Bibil, W.: SETHEO ? a high-performance theorem prover, J. Symbolic Computation 15(5/6) (1992), 183-212. · Zbl 0759.68080
[30] Fuchs, M. and Wolf, A.: System description ? Cooperation in model elimination: CPTHEO, in C. Kirchner and H. Kirchner (eds.), Proc. 15th Int. Conf. on Automated Deduction, LNCS 1421, Springer-Verlag, 1998, pp. 42-46.
[31] Schumann, J. and Letz, R.: PARTHEO: A high performance parallel theorem prover, in M. E. Stickel (ed.), Proc. 10th Int. Conf. on Automated Deduction, LNAI 449, Springer-Verlag, 1990, pp. 40-56. · Zbl 0708.68076
[32] Bose, S., Clarke, E. M., Long, D. E. and Michaylov, S.: PARTHENON: A parallel theorem prover for non-Horn clauses, J. Automated Reasoning 8(2) (1992), 153-181. · Zbl 0759.68079
[33] Astrachan, O.: METEOR: Exploring model elimination theorem proving, J. Automated Reasoning 13(3) (1994), 283-296. · Zbl 00724132
[34] Astrachan, O. L. and Loveland, D. W.: METEORs: High performance theorem provers using model elimination, in R. S. Boyer (ed.), Automated Reasoning: Essays in Honor of Woody Bledsoe, Kluwer, 1991, pp. 31-60.
[35] MacIntosh, D. J., Conry, S. E. and Meyer, R. A.: Distributed automated reasoning: Issues in coordination, cooperation and performance, IEEE Trans. Systems, Man, Cybernet. 21(6) (1991), 1307-1316.
[36] Denzinger, J., Kronenburg, M. and Schulz, S.: DISCOUNT ? a distributed and learning equational prover, J. Automated Reasoning 18(2) (1997), 189-198. · Zbl 05468571
[37] Denzinger, J. and Fuchs, D.: Cooperation of heterogeneous provers, in T. Dean (ed.), Proc. of the 16th Int. Joint Conf. on Artificial Intelligence, Stockholm, Sweden, July 31?August 6, Morgan Kaufmann, 1999, pp. 10-15.
[38] Weidenbach, C.: Spass: Version 0.49, J. Automated Reasoning 18(2) (1997), 247-252. · Zbl 05468578
[39] Suttner, C. B.: SPTHEO ? A parallel theorem prover, J. Automated Reasoning 18(2) (1997), 253-258. · Zbl 05468579
[40] Suttner, C. B.: SPS-Parallelism+SETHEO=SPTHEO, J. Automated Reasoning 22(4) (1999), 397-431. · Zbl 0929.68111
[41] Wolf, A.: p-SETHEO: Strategy parallelism in automated theorem proving, in H. de Swert (ed.), Proc. Int. Conf. TABLEAUX?98: Analytic Tableaux and Related Methods, LNAI 397, Springer-Verlag, 1998, pp. 320-324.
[42] Schumann, J.: SiCoTHEO ? Simple competitive parallel theorem provers based on SETHEO, in J. Geller, H. Kitano and C. B. Suttner (eds.), Parallel Processing for Artificial Intelligence 3, Elsevier, 1997, pp. 231-245.
[43] Sutcliffe, G. and Seyfang, D.: Smart selective competition parallelism ATP, in A. Kumar and I. Russell (eds.), Proc. 12th Florida Artificial Intelligence Research Symposium, Orlando, FL, May 3-5, American Association for Artificial Intelligence Press, 1999, pp. 341-345.
[44] De Nivelle, H.: Bliksem 1.00, in C. Kirchner and H. Kirchner (eds.), Proc. 15th Int. Conf. on Automated Deduction, Lindau, Germany, July 5-10, LNCS 1421, Springer-Verlag, 1998, p. 9.
[45] Tammet, T.: Gandalf, J. Automated Reasoning 18(2) (1997), 247-252. · Zbl 05468572
[46] McCune, W.: Otter 3.3 Reference Manual, Technical Memorandum No. 249, Mathematics and Computer Science Division, Argonne National Laboratory, 2001 (http://www-unix.mcs.anl.gov/AR/mace2/mace2.pdf).
[47] http://www.cs.miami.edu/\(\sim\)tptp/CASC/16/
[48] Newborn, M.: The Great Theorem Prover, Newborn Software, 1989.
[49] http://www.cs.miami.edu/\(\sim\)tptp/CASC/19/
[50] Geist, A., Beguelin, A., Dongarra, J., Jiang, W., Manchek, R. and Sunderam, V.: PVM: Parallel Virtual Machine, MIT Press, 1994. · Zbl 0849.68032
[51] Draeger, J.: Anwendung des Theorembeweisers SETHEO auf angeordnete Körper, FKI-186-93, Technische Universität München, Munich, 1993.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.