We present an experimental system strongly inspired by miniKanren, implemented on top of the tactics mechanism of the HOL~Light theorem prover. Our tool is at the same time a mechanism for enabling the logic programming style for reasoning and computing in a theorem prover, and a framework for writing logic programs that produce solutions endowed with a formal proof of correctness.
Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System / Marco Maggesi; Massimo Nocentini. - ELETTRONICO. - (2020), pp. 0-0. [10.48550/arXiv.2007.04691]
Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System
Marco Maggesi;Massimo Nocentini
2020
Abstract
We present an experimental system strongly inspired by miniKanren, implemented on top of the tactics mechanism of the HOL~Light theorem prover. Our tool is at the same time a mechanism for enabling the logic programming style for reasoning and computing in a theorem prover, and a framework for writing logic programs that produce solutions endowed with a formal proof of correctness.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
2007.04691v1.pdf
accesso aperto
Tipologia:
Pdf editoriale (Version of record)
Licenza:
Creative commons
Dimensione
526.29 kB
Formato
Adobe PDF
|
526.29 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
