CINECA IRIS Institutional Research Information System
IRIS è l’archivio della produzione scientifica della Fondazione Bruno Kessler.
EnglishA 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
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte di FBK.
| Titolo: | Program Tactics and Logic Tactics | |
| Autori: | ||
| Data di pubblicazione: | 1996 | |
| Rivista: | ||
| 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 | |
| Handle: | http://hdl.handle.net/11582/977 | |
| Appare nelle tipologie: | 1.1 Articolo in rivista |
File in questo prodotto:
http://hdl.handle.net/11582/977
Copyright © 2021