Journal of Mathematical Sciences

, Volume 126, Issue 3, pp 1182–1194 | Cite as

Solution lifting method for handling meta-variables in TH∃OREM∀

  • B. Konev
  • T. Jebelean


We approach the problem of finding witnessing terms in proofs by the method of meta-variables. We describe an efficient method for handling meta-variables in natural style proofs and its implementation in the TH∃OREM∀ system. The method is based on a special technique for finding meta-substitutions when the proof search is performed in an AND-OR deduction tree. The implementation does not depend on the search strategy and allows easy integration with various special provers as well as with special unification/solving engines. We demonstrate the use of this method in the context of a special forward/backward inference strategy for producing proofs in elementary analysis. Bibliography: 28 titles.


Search Strategy Efficient Method Special Technique Easy Integration Inference Strategy 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Hähnle and P. Schmitt, “The liberalized δ-rule in free variable semantic tableaux,” J. Automat. Reason., 13(2), 211–221 (1994).Google Scholar
  2. 2.
    P. Baumgartner, N. Eisinger, and U. Furbach, “A confluent connection calculus,” in: CADE 99 (1999), pp. 329–343.Google Scholar
  3. 3.
    B. Beckert and R. Hähnle, “Analytic tableaux,” in: Automated Deduction - a Basis for Applications, Vol. 1, W. Bibel and P. Schmitt (eds.), Kluver Academic Publishers (1998), pp. 11–41.Google Scholar
  4. 4.
    B. Beckert, “Depth-first proof search without backtracking for free variable semantic tableaux,” Technical Report 99-1, 33–54 (1999).Google Scholar
  5. 5.
    M. Beeson, “Automatic derivation of the irrationality of e,” Electron. Notes Theor. Comput. Science, 23(3) (2001), Scholar
  6. 6.
    W. Bibel, Automated Theorem Proving, 2nd edition, Vieweg, Braunschweig (1987).Google Scholar
  7. 7.
    W. Bibel and P. Schmitt (eds.), Automated Deduction - a Basis for Applications, Vols. 1–3, Kluver Academic Publishers (1998).Google Scholar
  8. 8.
    K. Broda. “The relationship between semantic tableau and resolution theorem proving,” in: Proceedings of Workshop on Logic, Debrecen, Hungary (1980).Google Scholar
  9. 9.
    F. M. Brown, “Toward the automation of set theory and its logic,” Artificial Intelligence, 10, 281–316 (1978).Google Scholar
  10. 10.
    B. Buchberger, “Using Mathematica for doing simple mathematical proofs,” in: Proceedings of the 4th International Mathematica users’ conference (Tokyo), Wolfram Media Publishing (1996), pp. 80–96.Google Scholar
  11. 11.
    B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, and W. Windsteiger, “Theorema: A progress report,” Technical Report 99-42, Research Institute for Symbolic Computation (1999).Google Scholar
  12. 12.
    B. Buchberger and T. Jebelean, “The predicate logic prover,” in: Proceedings of the First International Theorema Workshop, RISC Linz report series, No. 97-20, Research Institute for Symbolic Computation (1997).Google Scholar
  13. 13.
    B. Buchberger, T. Jebelean, F. Kriftner, M. Marin, E. Tomuta, and D. Vasaru, “A survey of the Theorema project,” in: Proceedings of ISSAC’97 (International Symposium on Symbolic and Algebraic Computation), W. Kuechlin (ed.), Maui, Hawaii (1997).Google Scholar
  14. 14.
    B. Buchberger and E. Tomuta, “Combining provers in the theorema system,” Technical report 98-02, Research Institute for Symbolic Computation (1998).Google Scholar
  15. 15.
    G. V. Davydov, S. Yu. Maslov, G. E. Mints, V. P. Orevkov, and A. O. Slisenko, “A computer algorithm for the determination of deducibility on the basis of the inverse method,” in: Automation of reasoning. 2. Classical papers on computational logic, 1967–1970, J. Siekmann and G. Wrightson (eds.), Springer-Verlag (1983), pp. 531–541.Google Scholar
  16. 16.
    A.I. Degtyarev, A.V. Lyaletski, and M.K. Morokhovets, “Evidence algorithm and sequent logical inference search,” Lect. Notes Comput. Sci., 1705, 44–61 (1999).Google Scholar
  17. 17.
    M. Fitting, First-Order Logic and Automated Theorem Proving, 2nd edition, Springer (1996).Google Scholar
  18. 18.
    G. Gentzen, “Untersuchungen über das logische schließ,” Math. Z., 39, 176–210, 405–433 (1934).Google Scholar
  19. 19.
    M. Giese, “Incremental closure of free variable tableaux,” to appear in Lect. Notes Comput. Sci. Google Scholar
  20. 20.
    M. Giese, “Proof search without backtracking using instance streams, position paper,” in: Proceedings of the International Workshop on First-Order Theorem Proving, St. Andrews, Scotland (2000).Google Scholar
  21. 21.
    C. Kanger, “A simplified proof method for elementary logic,” in: Computer Programming and Formal Systems, North-Holland, Amsterdam (1963), pp. 87–94.Google Scholar
  22. 22.
    B. Konev and T. Jebelean, “Using meta-variables for natural deduction in theorema,” in: Calculemus 2000: Integration of Symbolic Computation and Mechanized Reasoning, M. Kerber and M. Kohlhase (eds.), A. K. Peters, Natik, Massatchussets (2000).Google Scholar
  23. 23.
    J. Krajíček and P. Pudlák, “The number of proof lines and size of proofs in first order logic,” Arch. Math. Logic, 27, 69–84 (1988).Google Scholar
  24. 24.
    E. Melis and V. Sorge, “Employing external reasoners in proof planning,” Electron. Notes Theor. Comput. Sci., 23(3) (2001), Scholar
  25. 25.
    V. P. Orevkov, Complexity of Proofs and Their Transformations in Axiomatic Theories, Amer. Math. Soc. (1993).Google Scholar
  26. 26.
    D. Prawitz, “An improved proof procedure,” Theoria, 26, 102–139 (1960).Google Scholar
  27. 27.
    A. Robinson and A. Voronkov, Handbook of Automated Reasoning, Elsevier (2001).Google Scholar
  28. 28.
    H. Wang, “Toward mechanical mathematics,” IBM J. Res. Develop., 4(1), 2–22 (1960).Google Scholar

Copyright information

© Springer Science+Business Media, Inc. 2005

Authors and Affiliations

  • B. Konev
  • T. Jebelean

There are no affiliations available

Personalised recommendations