Logic-Based Program Synthesis and Transformation
Logic-Based Program Synthesis and Transformation
复制标题
基于逻辑的程序合成和转换
DOI：
10.1007/978-3-319-27436-2_6
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Fu P
中科院分区：
文献类型：
--
作者：
Fu P
我们提出了一种新的类型理论方法SLD-归结和霍恩子句逻辑编程。它将Horn公式视为类型，并将给定查询的派生视为查询给定类型的居民（证明项）的构造。我们提出了一种程序转换的方法，允许转换逻辑程序的方式证明证据一起SLD推导计算。我们讨论了这种方法的两个应用：在最近提出的生产力理论的结构分辨率，并在类型类推断。
We propose a new type-theoretic approach to SLD-resolution and Horn-clause logic programming. It views Horn formulas as types, and derivations for a given query as a construction of the inhabitant (a proof-term) for the type given by the query. We propose a method of program transformation that allows to transform logic programs in such a way that proof evidence is computed alongside SLD-derivations. We discuss two applications of this approach: in recently proposed productivity theory of structural resolution, and in type class inference.
类型化逻辑程序的模式分析域
影响因子：
2
作者：
J. Smaus;P. Hill;A. King
通讯作者：
A. King