Program tactics and logic tactics

  • Fausto Giunchiglia
  • Paolo Traverso
  • Mechanized Reasoning Group
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 822)


In the past, tactics have been mostly implemented as programs written in some programming language, e.g. ML. We call the tactics of this kind, Program Tactics. In this paper we present a first order classical metatheory, called MT, with the following properties: (1) tactics are terms of the language of MT. We call these tactics, Logic Tactics; (2) there exists a mapping between Logic Tactics and the Program Tactics implemented within the GETFOL theorem prover. Property (1) allows us to use GETFOL to prove properties of and to build new Logic Tactics. Property (2) can be exploited to perform a bidirectional translation between Logic Tactics and Program Tactics.


Inference Rule Sequent Tree Theorem Prover Function Symbol Predicate Symbol 
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.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1979. ACM monograph series.Google Scholar
  2. 2.
    R.S. Boyer and J.S. More. A theorem prover for a computational logic. In Proceedings of the 10th Conference on Automated Deduction, Lecture Notes in Computer Science 449, Springer-Verlag, pages 1–15, 1990.Google Scholar
  3. 3.
    A. Bundy. The Use of Explicit Plans to Guide Inductive Proofs. In R. Luck and R. Overbeek, editors, Proc. of the 9th Conference on Automated Deduction, pages 111–120. Springer-Verlag, 1988. Longer version available as DAI Research Paper No. 349, Dept. of Artificial Intelligence, Edinburgh.Google Scholar
  4. 4.
    R. Cartwright and J. McCarthy. Recursive Programs as Functions in a First Order Theory, March 1979. SAIL MEMO AIM-324. Also available as CS Dept. Report No. STAN-CS-79-17.Google Scholar
  5. 5.
    R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986.Google Scholar
  6. 6.
    A. Felty. Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language. To appear in: Journal of Automated Reasoning, 1993.Google Scholar
  7. 7.
    A. Felty and D. Miller. Specifying Theorem Provers in a Higher-Order Logic Programming Language. In R. Luck and R. Overbeek, editors, Proc. of the 9th Conference on Automated Deduction, pages 61–80. Springer-Verlag, 1988.Google Scholar
  8. 8.
    F. Giunchiglia. The GETFOL Manual — GETFOL version 1. Technical Report 92-0010, DIST — University of Genova, Genoa, Italy, 1992.Google Scholar
  9. 9.
    F. Giunchiglia and A. Armando. A Conceptual Architecture for Introspective Systems. Forthcoming IRST-Technical Report, 1993.Google Scholar
  10. 10.
    F. Giunchiglia and A. Cimatti. Introspective Metatheoretic Reasoning. In Proc. of META-94, Workshop on Metaprogramming in Logic, Pisa, Italy, June 19–21, 1994. Also IRST-Technical Report 9211-21, IRST, Trento, Italy.Google Scholar
  11. 11.
    F. Giunchiglia and P. Traverso. Reflective reasoning with and between a declarative metatheory and the implementation code. In Proc. of the 12th International Joint Conference on Artificial Intelligence, pages 111–117, Sydney, 1991. Also IRST-Technical Report 9012-03, IRST, Trento, Italy.Google Scholar
  12. 12.
    F. Giunchiglia and P. Traverso. A Metatheory of a Mechanized Object Theory. Technical Report 9211-24, IRST, Trento, Italy, 1992. Submitted for publication to: Journal of Artificial Intelligence.Google Scholar
  13. 13.
    J. Goguen. Higher-order functions considered unnecessary for higher-order programming. In D. A. Turner, editor, Research Topics in Functional Programming, pages 309–351. Addison Wesley, 1990.Google Scholar
  14. 14.
    J. Goguen, A. Stevens, H. Hilbrdink, and K. Hobley. 2OBJ: a metalogical framework theorem prover based on equational logic. Phil. Trans. R. Soc. Lond., 339:69–86, 1992.Google Scholar
  15. 15.
    J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J. Jouannaud. Introducing OBJ. In J. Goguen, D. Coleman, and R.Gallimore, editors, Applications of algebraic specification using OBJ. Cambridge, 1992.Google Scholar
  16. 16.
    M.J. Gordon, A.J. Milner, and C.P. Wadsworth. Edinburgh LCF — A mechanized logic of computation, volume 78 of Lecture Notes in Computer Science. Springer Verlag, 1979.Google Scholar
  17. 17.
    M.J. Gordon, R. Milner, L. Morris, and C. Wadsworth. A Metalanguage for Interactive Proof in LCF. CSR report series CSR-16-77, Department of Artificial Intelligence, Dept. of Computer Science, University of Edinburgh, 1977.Google Scholar
  18. 18.
    D. J. Howe. Computational metatheory in Nuprl. In R. Lusk and R. Overbeek, editors, CADE9, 1988.Google Scholar
  19. 19.
    Z. Manna. Mathematical Theory of Computation. McGraw-Hill, New York, 1974.Google Scholar
  20. 20.
    L. Paulson. Tactics and Tacticals in Cambridge LCF. Technical Report 39, Computer Laboratory, University of Cambridge, 1979.Google Scholar
  21. 21.
    L. Paulson. The Foundation of a Generic Theorem Prover. Journal of Automated Reasoning, 5:363–396, 1989.Google Scholar
  22. 22.
    Lawrence C. Paulson. A Higher-Order Implementation of Rewriting. Science of Computer Programming, 3:119–149, 1983.Google Scholar
  23. 23.
    D. Prawitz. Natural Deduction — A proof theoretical study. Almquist and Wiksell, Stockholm, 1965.Google Scholar
  24. 24.
    R.W. Weyhrauch. Prolegomena to a Theory of Mechanized Formal Reasoning. Artif. Intell., 13(1):133–176, 1980.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Fausto Giunchiglia
    • 1
    • 2
  • Paolo Traverso
    • 1
  • Mechanized Reasoning Group
  1. 1.IRST-Istituto per la Ricerca Scientifica e TecnologicaPovoItaly
  2. 2.University of TrentoTrentoItaly

Personalised recommendations