论文标题
Kanren Light：动态认证的交互式逻辑编程系统
Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System
论文作者
论文摘要
我们提出了一个强烈灵感的实验系统，该系统受到Minikanren的启发，该系统是基于Hol〜light Theorem Prover的策略机制实现的。同时，我们的工具是一种机制，用于启用定理供仪中推理和计算的逻辑编程样式的机制，以及编写逻辑程序的框架，以产生具有正式证明的解决方案的逻辑程序。
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.
