Jul, 2010

具有 Cut 操作的逻辑程序自动终止分析

PDF
TL;DR本文介绍了一种新的预处理方法，将 Prolog 程序自动转换为无割程序，进而证明定义逻辑程序的终止性，该方法已应用于终止证明器 AProVE 并取得成功。
terminationlogic programsprologcut-free programaprove
发现论文，激发创造
  • 通过术语重写自动终止逻辑程序的证明

    本文介绍了通过改良变换法来解决逻辑程序终止性分析的限制的方法，并将其应用于 AProVE 终止证明器进行实验与评估。

    Mar, 2008

  • 使用线性约束进行逻辑编程的终止分析

    这篇论文提出了规则受限和循环受限程序的新类别，通过更全局地分析术语如何从规则的主体传播到头部来克服目前方法的各种限制。

    Dec, 2015

  • 检查逻辑程序使用函数符号的自下而上求值的终止性

    本篇论文研究了带有函数符号的逻辑程序在底部向上计算过程中的终止问题，并提出了 Gamma-acyclicity 和安全性等可判定的规则，同时阐述了这些规则在限制查询中的应用及程序的层次结构。

    Jul, 2014

  • 紧凑逻辑程序

    本论文探讨否定作为失败的两种理论之间的关系：基于程序完成和基于稳定模型或答案集。研究表明，当一个逻辑程序满足一定的语法条件 (被称为 “紧密性”) 时，它的稳定模型可以被表征为其完成模型。本研究将 “紧密性” 的定义和 Fages 的定理扩展到规则体中包含嵌套表达式的程序，并研究包含谓词的传递闭包定义的紧致逻辑程序。

    Feb, 2003

  • 优先逻辑编程的两个结果

    本文探讨了优先默认推理的两个特性，揭示了优先逻辑程序的互斥性和唯一性之间的密切关系，并探讨了将扩展逻辑程序的分裂技术推广到优先逻辑程序的可能性，证明了可以在一定条件下简化优先逻辑程序的评估。

    Mar, 2002

  • 针对逻辑程序的定制简化超级自然推理体系的增量维护

    介绍了使用优化的过程生成一系列单调增长的命题程序的新策略，这些命题程序可以更新和重复使用，因此结合后续输入会降低更新成本，特别是在后期迭代中，并报道了 OPT 的实现和性能，是 TPLP 的待考虑论文。

    Aug, 2020

  • 逻辑程序的二进制化和部分推导加速

    该论文介绍了二进制逻辑程序的产生，以及如何通过部分归纳法来改善在类似的程序中引入的延续变量。通过将其转化为二进制逻辑程序，使用部分归纳法，能够得到一个更加高效的计算行为。

    Dec, 2003

  • 由 (条件) 终止证明驱动的资源分析

    该论文提出了一种资源分析方法，它使用终止分析结果驱动成本关系系统（CRS）的生成，并且最终生成的线性有界 CRS（LB-CRS）克服了现有技术产生复杂程序流程的成本函数难以解决的问题，作者还制定了一种名为 MaxCore 的资源分析工具，并针对 C 整数程序的一组基准测试进行了实验，结果显示 MaxCore 优于其他所有资源分析工具。

    Jul, 2019

  • 通过正定证明终止概率程序的分析

    针对非确定性概率程序的终止性质，提出了基于多项式守卫和分配的终止分析方法，通过 Positivstellensatz 的方法综合多项式级别超级马丁格斯来证明其终止性，并且还可以合成二次排名超级马丁格斯来处理复杂的程序。

    Apr, 2016

  • 非分层逻辑程序的稳定模型存在性

    该论文介绍了一个基础性的结果，给出了一种稳定模型的存在条件的句法特征表示，利用引入新的规范形式和循环依赖来定义稳定模型元语，从而保证了稳定模型存在的确定性。

    Dec, 2004