Functions as types or the "Hoare logic" of functional dependencies
受程序设计理论统一化趋势的启发，本文说明了标准数据依赖理论的代数处理如何为关系数据配备函数类型和相关类型系统，这对数据库操作的类型检查和查询优化是有用的。这种类型化的方法，数据库编程，然后被证明是同一个家庭的其他编程逻辑，如例如。霍尔逻辑或最强不变函数的逻辑，用于分析while语句。使用自动演绎系统，如Prover9的类型检查和查询优化上这样一个代数方法的前景被认为是。
2012-10-17 cs.LO
Refinement Type Directed Search for Meta-Interpretive-Learning of Higher-Order Logic Programs
University of Oxford（牛津大学）；St. John’s College（圣约翰学院）
在归纳逻辑程序设计（ILP）社区中的程序合成问题通常被视为无类型的。我们考虑了用户提供的类型对背景知识的好处。在元解释学习（MIL）框架的基础上，我们证明了类型检查能够修剪程序的大部分假设空间。引入多态类型检查的MIL方法逻辑程序合成验证强有力的理论和实验结果，显示了立方减少的搜索空间和合成时间的大小，在类型化的背景谓词的数量。此外，我们能够推断多态类型的合成条款和整个程序。另一个进步是开发了一种在ILP中利用精化类型的方法。在这里，我们表明，进一步修剪的搜索空间可以实现，虽然SMT解决用于细化类型检查来
2021-02-18 cs.AI cs.LO
Autonomous Task Completion Based on Goal-directed Answer Set Programming
本研究针对自主智能体任务规划的可解释性与可靠性问题，提出结合归纳学习与目标导向回答集编程的方法，开发了基于s(CASP)的Python工具并探索模拟任务完成中复杂问题的解决方案。
2025-02-13 cs.LO cs.SE
On Zeno-like Behaviors in the Event Calculus with Goal-directed Answer Set Programming
Brno University of Technology（布尔诺理工大学）；CETINIA, Universidad Rey Juan Carlos（雷乌斯·胡安·卡洛斯大学 CETINIA）；UT Dallas（德州大学达拉斯分校）；Ardent Innovation Labs（Ardent 创新实验室）；Multitude Corp.（Multitude 公司）；Honeywell International s.r.o.（霍尼韦尔国际有限公司）；Masaryk University（马萨里克大学）
本文研究了事件演算中因连续时间表示导致的芝诺行为问题，提出通过目标导向的答案集编程处理此类行为的方法，并提出自动检测此类情况的技术。
2026-01-07 cs.LO
Beyond Lemma Sharing -- Novel Parallelization Strategies for Property Directed Reachability
Huawei Technologies Switzerland AG（华为瑞士技术有限公司）
针对PDR并行化可扩展性难题，提出抢占式传播和ARPOS两种新策略，并在rIC3上验证，显著优于经典引理共享。
2026-09-09 cs.DC cs.LO cs.PL
Property Directed Reachability for Generalized Petri Nets
我们提出了一个半决策过程检查广义可达性，广义Petri网，这是基于属性导向可达性（PDR）方法。我们实际上定义了三个不同的版本，这取决于用于提取可能的证人的方法，并且能够处理越来越困难的问题。我们已经实现了我们的方法在一个模型检查器称为SMPT，并给出经验证据，我们的方法可以处理的问题，是困难的或不可能检查与当前最先进的工具。
2022-08-05 cs.LO
Flexible graph matching and graph edit distance using answer set programming
图同构、子图同构和图编辑距离问题是一类有着广泛应用的组合问题。启发式的精确和近似算法，这些问题中的每一个已经开发了不同种类的图形：有向，无向，标记等，但是，额外的工作往往需要适应这种算法不同类别的图形，例如，以适应标签和属性注释的节点和边缘。在本文中，我们提出了一种基于答案集编程的方法。我们展示了如何定义这些问题中的每一个一般类的属性图有向边，标签和键值属性注释节点和边缘。我们评估这种方法的各种合成和现实的图形，证明它是可行的快速原型方法。
2019-11-26 cs.LO
Polymorphic Types in ACL2
本文介绍了一个工具套件的ACL 2程序设计语言，其中包括某些想法从欣德利-米尔纳范式的函数式编程（如流行的语言，如ML和Haskell），包括一个“类型化”的编程风格的能力，定义多态类型。这些思想通过宏引入到ACL 2语言中，利用ACL 2的保护检查机制对函数定义和定理进行类型检查。最后，我们将讨论如何使用这些宏来实现Specware，软件规范和实现系统的功能。
2014-06-06 cs.LO cs.PL
Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification
本文通过为{log}语言定义类型系统并实现类型检查器，将类型检查与集合约束求解结合，提高了软件验证的自动化程度，并通过两个工业案例验证了其有效性。
2024-03-21 cs.LO cs.PL
SMT-based Symbolic Model-Checking for Operator Precedence Languages
针对现有POTL显式状态模型检测方法可扩展性差的问题，本文提出首个基于SMT的符号化方法，将POTL公式与程序模型编码为SMT公式，通过求解器以有界模型检测方式搜索反例轨迹，实验验证了方案有效性。
2024-05-18 cs.LO
Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming
CETINIA Universidad Rey Juan Carlos（胡安卡洛斯国王大学CETINIA）；IMDEA Software Institute（IMDEA软件研究所）；Universidad Politécnica de Madrid（马德里理工大学）；University of Texas at Dallas（德克萨斯大学达拉斯分校）
自动常识推理对于构建具有可解释AI等特征的类人AI系统至关重要。事件演算（EC）是一个形式主义的家庭，模型常识推理与健全的，逻辑基础。先前使用EC进行机械化推理的尝试在处理密集域中的连续变化（例如，时间和其他物理量）、变量之间的约束、默认否定以及不同推理方法的统一应用等。我们建议使用的s（CASP），查询驱动的，自上而下的执行模型的谓词答案集编程的约束，模型和原因使用EC。我们展示了如何EC的情况下，可以自然和直接编码的s（CASP），以及它如何使演绎和溯因推理任务的域具有约束，涉及密集的时间和密集的流畅性。
2021-06-28 cs.AI cs.LO
Disjunction and modular goal-directed proof search
本文研究了一阶多模态逻辑中的目标导向证明搜索。关键的问题是设计一个证明系统，尊重模块性和局部性的假设，许多模态逻辑。通过强制歧义被独立地考虑，特别是模块化的析取可以被用来构建有效的可执行规范的推理任务，涉及部分信息，否则可能需要禁止搜索。为了实现这一行为，需要事先证明理论的理由逻辑编程扩展，加强，并结合证明理论分析模态演绎以一种新的方式。
2002-06-05 cs.LO
Eliminating Unfounded Set Checking for HEX-Programs
Technische Universität Wien（维也纳工业大学）
HEX程序是应答集编程（ASP）范例的扩展，其通过所谓的外部原子将外部计算手段并入声明性程序设计语言中。它们的语义是根据Faber-Leone-Pfeifer（FLP）约简的最小模型定义的。开发本地解算器的HEX程序的基础上适当的概念，无根据的集合一直受到最近的研究效率的原因。虽然这导致了使用FLP约简的朴素最小性检查的改进，但对发现性的测试仍然是一项计算昂贵的任务。在这项工作中，我们提高了在这方面的HEX程序评估确定的语法类的程序，可以有效地识别，并允许完全跳过的foundedness检查。此外，我们开发的标准分解成组件的程序，这样的搜索无根据集可以受到限制。观察到我们的结果适用于许多HEX程序的应用程序提供了分析证据，我们的方法的意义和有效性，这是补充了初步的实验验证的简要讨论。
2013-01-08 cs.AI cs.LO
A Theoretical Study of (Full) Tabled Constraint Logic Programming
表格约束逻辑编程（TCLP，tableed constraint logic programming）已经被证明比LP、CLP或LP with tabling更有表现力，在某些情况下更有效。在本文中，我们提供了关于语义，正确性，完整性和终止的自顶向下执行策略的完整TCLP，即，TCLP的特点是在呼叫和应答中进行蕴涵检查。我们提出了一个自顶向下的语义TCLP，并表明它是等价的不动点语义。我们研究了一个程序生成的约束如何有效地影响终止，即使是约束类，约束不紧，概括以前的结果。我们还介绍了不同的约束投影的变体如何影响TCLP实现的正确性和完整性。所有提出的特点都实现（或可以实验）在Mod TCLP，一个模块化的框架表约束逻辑编程，Ciao Prolog逻辑编程系统的一部分。
2020-09-28 cs.LO
Bounded LTL Model Checking with Stable Models
本文介绍了异步并发系统的有界模型检验，作为回答集编程的一个很有前途的应用领域。作为异步系统的通信自动机，1-安全Petri网的推广模型，使用。它示出了如何1-安全的Petri网和对网络的行为的要求可以被翻译成一个逻辑程序，这样的有界模型检验问题的网可以通过计算相应的程序的稳定模型来解决。稳定模型语义的使用导致有界可达性和死锁检测任务的紧凑编码，以及线性时序逻辑的有界模型检验的更一般的问题。给出了所设计的翻译的正确性证明，并给出了使用该翻译和Smodels系统的一些实验结果。
2003-05-23 cs.AI cs.LO
Automatic Verification of Timed Concurrent Constraint Programs
时间并发约束（Timed Concurrent Constraint，tccp）是并发约束编程（Concurrent Constraint Programming，cc）范式的扩展，它允许我们指定时间至关重要的并发系统，例如反应式系统。可以有无限多个状态的系统可以在tccp中指定。模型检验是一种能够自动验证具有大量状态的有限状态系统的技术。在过去的几年里，一些研究已经调查了如何扩展模型检验技术的系统具有无限数量的状态。在本文中，我们提出了一种方法，利用tccp的计算模型。基于约束的计算允许我们定义一种方法，将模型检验算法应用于（一类）无限状态系统。我们扩展的经典算法的模型检验LTL的一个特定的逻辑定义的验证tccp和tccp结构，我们在这项工作中定义的建模程序的行为。我们定义了一个限制的时间，以得到一个有限的模型，然后我们开发了一些说明性的例子。据我们所知，这是第一个为tccp定义模型检验方法的方法。
2005-05-11 cs.LO
Justifications for Goal-Directed Constraint Answer Set Programming
道德和法律问题使得有必要制定可能直接影响人们生活的计划（例如，法律或健康咨询），以人类可以理解的方式证明所提供的建议是合理的。答案集编程具有丰富的语义，可以非常简洁地表达复杂的知识。然而，证明为什么答案是ASP程序的结果可能是不平凡的--当用户是给定领域的专家，但不一定精通ASP时更是如此。大多数ASP系统生成的答案使用SAT解决程序的基本规则，不匹配人类如何感知推理。我们建议使用的（CASP），查询驱动的，自上而下的执行模型的谓词ASP的约束条件生成的理由树（约束）的答案集。s（CASP）的操作语义依赖于反向链接，这是直观的遵循，并有助于生成更容易翻译成自然语言的解释。我们如何（CASP）提供最小的理由，除其他外，在文献中提出的相关例子，既作为搜索树，但更重要的是，作为自然语言的解释。我们验证我们的设计与真正的ASP应用程序，并评估生成的成本（CASP）的理由树。
2020-09-22 cs.LO cs.PL
DAG-width of Control Flow Graphs with Applications to Model Checking
由结构化程序产生的控制流图的树宽最多为6。然而，由于控制流图本质上是有向的，因此考虑有向图的宽度度量是有意义的。我们使用所谓的DAG宽度，并表明，DAG宽度的控制流图所产生的结构化（goto自由）的程序是最多三个。此外，我们还给出了一个线性时间算法来计算这些控制流图的DAG分解。这个结果的一个结果是，奇偶游戏（因此$μ$ -演算模型检验问题），这是已知的有界DAG宽度的图上是易处理的，可以有效地解决在控制流图的实践。
2015-03-03 cs.DM cs.LO cs.PL
Knowledge-Assisted Reasoning of Model-Augmented System Requirements with Event Calculus and Goal-Directed Answer Set Programming
Honeywell Advanced Technology（霍尼韦尔先进技术公司）；The University of Texas at Dallas（德克萨斯大学达拉斯分校）；Honeywell International s.r.o（霍尼韦尔国际有限公司）；Brno Univ. of Technology（布尔诺理工大学）；Universidad Rey Juan Carlos（胡安卡洛斯国王大学）
我们认为，在约束自然语言的网络物理系统的要求。我们提出了新的自动化技术，以帮助这些要求的发展，使他们是一致的，可以承受感知故障。我们展示了如何使用事件演算（EC）来建模网络物理系统的需求，EC是AI中用于表示动作和变化的形式主义。我们还展示了如何回答集编程（ASP）及其查询驱动实现（CASP）可以用来直接实现的事件演算模型的需求。该事件演算模型可用于自动验证需求。由于ASP是一种表达知识表示语言，它也可以用来表示上下文知识的网络物理系统，这反过来，可以用来找到差距，他们的需求规格。我们说明了我们的方法，通过高度报警系统从航空电子领域。
2021-09-10 cs.AI cs.LO cs.SC
CurryCheck: Checking Properties of Curry Programs
我们提出CurryCheck，一个工具来自动测试的功能逻辑程序设计语言咖喱写的程序。CurryCheck执行单元测试以及通过一个或多个参数进行参数化的属性测试。在后一种情况下，CurryCheck通过系统地枚举测试用例来测试这些属性，以便对于较小的有限域，CurryCheck可以实际证明属性。可以在Curry模块中定义单元测试和属性，而无需导出。因此，它们对于记录源代码的预期语义也很有用。此外，CurryCheck还支持自动检查源程序中出现的规范和合同。因此，CurryCheck是一个有用的工具，有助于基于属性和规范的可靠和测试良好的声明性程序的开发。
2016-08-19 cs.LO cs.PL
Combining Static and Dynamic Contract Checking for Curry
静态类型系统通常不足以表达对函数调用的所有要求。因此，带有前置和后置条件的契约可以用来表达对操作的更复杂的约束。可以在运行时间检查协定，以确保仅使用合理的参数调用操作并返回预期的结果。虽然这种动态契约检查提供了更可靠的程序执行，但它需要执行时间，并可能导致程序崩溃，这些崩溃可能会在编译时用更高级的方法检测到。为了改善这种情况的声明性语言，我们提出了一种方法，结合静态和动态的合同检查的功能逻辑语言咖喱。基于函数式逻辑程序设计中契约检验的形式化模型，提出了一种在编译时自动检验契约的方法。如果合同验证成功，则可以省略对合同的动态检查。这种方法减少了执行时间，而不会降低可靠的程序执行。在最好的情况下，当所有契约都被静态验证时，它提供了对软件的信任，因为在程序执行期间不会发生由于违反契约而导致的崩溃。
2017-09-14 cs.LO cs.PL
User Guided Abductive Proof Generation for Answer Set Programming Queries (Extended Version)
Singapore Management University（新加坡管理大学）；University of Toulouse（图卢兹大学）
我们提出了一种方法，用于生成可能的证据的查询相对于一个给定的答案集编程（ASP）规则集使用的溯因过程中的空间的溯因是自动构建的输入规则。给定一组（可能是空的）用户提供的事实，我们的方法推断出任何额外的事实，可能需要的蕴涵的查询，然后输出这些额外的事实，而无需用户明确指定的所有abdibles的空间。我们还提出了一种方法来生成一组有向边对应的理由图的查询。此外，通过不同形式的隐式项替换，我们的方法可以考虑用户提供的事实，并适当修改溯因解。过去关于绑架的工作主要是基于目标导向的方法。然而，这些方法可能导致求解器不是真正声明性的。少得多的工作已经做了实现绑架在一个自自底向上的的求解器，如Clingo ASP求解器。我们描述了新的ASP程序，可以直接在Clingo中运行，产生的溯因解和有向边集，而无需修改底层的求解引擎。
2022-09-16 cs.AI cs.LO
Infinite Qualitative Simulations by Means of Constraint Programming
我们引入了一个基于约束的框架，研究无限的定性模拟关注的突发事件，如时间，空间，形状，大小，抽象成一个有限的定性关系。为了定义模拟，我们结合了约束，正式的背景知识与定性推理与适当的状态间的约束，制定使用线性时序逻辑。我们实现了这种方法在约束编程系统中的思想，从有界模型检验。由此产生的系统允许我们以一种简单的方式测试和修改问题规范，并结合各种知识方面。
2006-08-03 cs.AI cs.LO
Model Checking Temporal Properties of Recursive Probabilistic Programs
本文研究了递归概率程序（pPDA）针对 $ω$-可见下推语言的模型检测问题，给出了可判定性与复杂性结果，证明 CaRet 等逻辑可指定过程调用与返回匹配等结构化性质。
2023-12-14 cs.FL cs.LO
Orbit-finite linear programming
研究约束为轨道有限线性不等式组的线性规划推广，提出判定实数解存在性及计算目标函数极值的决策过程，并证明整数解情形不可判定。
2024-11-13 cs.FL cs.LO
A Constructive Semantic Characterization of Aggregates in ASP
本技术说明描述了一个单调和连续的不动点算子，用于计算具有聚合的程序的答案集。不动点运算符依赖于聚合解的概念。在一定条件下，该操作符的行为完全相同的三值直接后果操作符$Φ^{aggr}_P$聚合程序，独立提出Pelov等人。该操作符使我们能够密切联系的计算复杂性的答案集检查和答案集存在问题的检查解决方案的聚合程序的成本。最后，我们与其他建议的逻辑编程与聚集的运营商所描述的语义。出现在逻辑编程理论与实践（TPLP）中。
2006-02-08 cs.AI cs.LO cs.PL
Auto-Tuning High-Performance Programs Using Model Checking in Promela
本文提出利用模型检查中的反例加速高性能程序自动调优，以OpenCL程序为例，结合Promela和SPIN工具实现并验证了该方法。
2023-05-16 cs.DC cs.LO
Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming
Sabanci University（萨班哲大学）
我们提出了一种新的正式框架（称为3D-nCDC-ASP）表示和理由的基本方向之间的扩展对象在3维（3D）空间，使用答案集编程（ASP）。3D-nCDC-ASP扩展了Cardinal Directional Calculus（CDC），提供了一种新的默认约束类型，并将nCDC-ASP扩展到3D。3D-nCDC-ASP提供了一个灵活的平台，提供不同类型的推理：默认的非单调推理，检查对象之间3D基本方向上的一组约束的一致性，解释不一致性，以及推断缺失的CDC关系。我们证明了3D-nCDC-ASP的可靠性，并说明其实用性与应用程序。本文件正在考虑被TPLP接受。
2020-08-10 cs.AI cs.LO
Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence
University of Nebraska Omaha（内布拉斯加大学奥马哈分校）
本文在Here-and-There逻辑中用内涵函数刻画clingo和dlv中聚合程序的语义，并研究强等价性，提出归约为经典一阶逻辑的变换以支持自动化验证。
2024-12-14 cs.AI cs.LO
Reasoning about Qualitative Direction and Distance between Extended Objects using Answer Set Programming
Sabanci University（萨班哲大学）
在这篇论文中，我们介绍了一个新的形式化框架，表示和推理的定性方向和扩展对象之间的距离关系，使用答案集编程（ASP）。我们以基数方向演算（CDC）为出发点，并扩展CDC与新的种类的约束，其中涉及默认值，偏好和否定。我们将此扩展版本称为nCDC。然后通过扩充定性距离关系对nCDC进行了进一步的扩展，并将其命名为nCDC+。对于CDC，nCDC，nCDC+，我们引入了一个基于ASP的通用框架来解决一致性检查问题，解决定性空间关系的组合和反转，推断对象之间未知或缺失的关系，并找到一个合适的配置，满足给定的查询对象。
2019-09-18 cs.AI cs.LO cs.RO
