二阶Horn片段的SLD-归结化简——技术报告——
计算机科学中的逻辑
2019-02-27 v1
摘要
我们提出SLD-归结的推导化简问题，即寻找一组子句的一个有限子集，使得使用该子集可通过SLD-归结推导出整个子句集，这是一个不可判定问题。我们研究了二阶Horn逻辑各片段的可化简性，并特别应用于归纳逻辑程序设计。我们还讨论了这些结果如何推广至标准归结。
引用
@article{arxiv.1902.09900,
title = {SLD-Resolution Reduction of Second-Order Horn Fragments -- technical report --},
author = {Sophie Tourret and Andrew Cropper},
journal= {arXiv preprint arXiv:1902.09900},
year = {2019}
}
备注
technical report, extends a conference paper accepted at JELIA 2019 with detailed proofs