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 tactics
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11582/977
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact