A tactic is any procedure which implements a correct search strategy. The goal of this paper is to provide a uniform framework where the user can hand-code tactics as programs in a metalevel programming language, can theorem prove them as terms in a first order classical metatheory, and is provided with a mechanism which allows for a bidirectional `translation` between the programming language and the logic. We call tactics of the first kind, `Program tactics`, those of the second kind `Logic tactics`. Inside this framework it is possible to use program tactics as terms inside Logic tactics and, viceversa, to use Logic tactics as programs inside Program tactics
Program Tactics and Logic Tactics
Giunchiglia, Fausto;Traverso, Paolo
1996
Abstract
A tactic is any procedure which implements a correct search strategy. The goal of this paper is to provide a uniform framework where the user can hand-code tactics as programs in a metalevel programming language, can theorem prove them as terms in a first order classical metatheory, and is provided with a mechanism which allows for a bidirectional `translation` between the programming language and the logic. We call tactics of the first kind, `Program tactics`, those of the second kind `Logic tactics`. Inside this framework it is possible to use program tactics as terms inside Logic tactics and, viceversa, to use Logic tactics as programs inside Program tacticsI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
