Abstract
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.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
R.S. Boyer and J.S. Moore. A Computational Logic. Academic Press, 1979. ACM monograph series.
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.
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.
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.
R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986.
A. Felty. Implementing Tactics and Tacticals in a Higher-Order Logic Programming Language. To appear in: Journal of Automated Reasoning, 1993.
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.
F. Giunchiglia. The GETFOL Manual — GETFOL version 1. Technical Report 92-0010, DIST — University of Genova, Genoa, Italy, 1992.
F. Giunchiglia and A. Armando. A Conceptual Architecture for Introspective Systems. Forthcoming IRST-Technical Report, 1993.
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.
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.
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.
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.
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.
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.
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.
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.
D. J. Howe. Computational metatheory in Nuprl. In R. Lusk and R. Overbeek, editors, CADE9, 1988.
Z. Manna. Mathematical Theory of Computation. McGraw-Hill, New York, 1974.
L. Paulson. Tactics and Tacticals in Cambridge LCF. Technical Report 39, Computer Laboratory, University of Cambridge, 1979.
L. Paulson. The Foundation of a Generic Theorem Prover. Journal of Automated Reasoning, 5:363–396, 1989.
Lawrence C. Paulson. A Higher-Order Implementation of Rewriting. Science of Computer Programming, 3:119–149, 1983.
D. Prawitz. Natural Deduction — A proof theoretical study. Almquist and Wiksell, Stockholm, 1965.
R.W. Weyhrauch. Prolegomena to a Theory of Mechanized Formal Reasoning. Artif. Intell., 13(1):133–176, 1980.
Author information
Authors and Affiliations
Consortia
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giunchiglia, F., Traverso, P., Mechanized Reasoning Group. (1994). Program tactics and logic tactics. In: Pfenning, F. (eds) Logic Programming and Automated Reasoning. LPAR 1994. Lecture Notes in Computer Science, vol 822. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58216-9_26
Download citation
DOI: https://doi.org/10.1007/3-540-58216-9_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58216-8
Online ISBN: 978-3-540-48573-5
eBook Packages: Springer Book Archive