Solving non-linear Horn clauses using a linear Horn clause solver
在本文中，我们表明，检查可满足性的一组非线性霍恩条款（也称为非线性霍恩条款计划）可以实现使用求解器的线性霍恩条款。我们实现这一点，通过交错的程序转换与线性霍恩条款（也称为线性霍恩条款求解器）的可满足性检查。程序转换是基于树维度的概念，我们将其应用于一组非线性子句，产生一组其派生树具有有界维度的集合。这样一套条款可以线性化。然后，主要的算法进行应用线性化变换和求解器的线性霍恩条款的一系列条款的连续增加的维度范围。然后，通过使用较低维度的条款解决方案来（部分）线性化较高维度的条款，进一步发展了该方法。我们构建了一个原型实现这种方法，并进行了一些实验上的一组验证问题，这表明了一些承诺。
2016-07-15 cs.LO cs.PL
Analysis and Transformation of Constrained Horn Clauses for Program Verification
本文综述了最近的工作应用分析和转换技术，起源于约束逻辑编程（CLP）领域的问题，验证软件系统。我们提出了基于专业化的技术翻译验证问题，为不同的程序设计语言，并在一般的软件系统，到满足性问题的约束霍恩条款（CHCs），一个术语，已成为流行的验证领域，指CLP程序。然后，我们描述了静态分析技术的CHCs，可用于推断相关的程序属性，如循环不变。我们还概述了一些转换技术的基础上专业化和折叠/展开规则，这是有用的，以提高CHC可满足性工具的有效性。最后，我们讨论了应用这些技术的未来发展。
2021-08-02 cs.LO cs.PL
Redundancy in Logic II: 2CNF and Horn Propositional Formulae
我们报告的复杂性结果的冗余公式的2CNF形式。我们首先考虑的问题，检查冗余，并显示一些算法，略优于平凡的。然后，我们分析了相关的问题，找到非冗余等价子集（I.E.S.）一个给定的集合。循环性的概念被证明与这些问题的复杂性有关。给出了Horn公式的一些结果。
2005-06-21 cs.AI cs.LO
Horn Fragments of the Halpern-Shoham Interval Temporal Logic (Technical Report)
我们调查的Halpern-Shoham区间时序逻辑的霍恩片段的可满足性问题取决于类型（盒或钻石）的区间模态算子，类型的基本线性顺序（离散或密集），和类型的语义的区间关系（自反或非自反）。例如，我们证明了对于任何类型的线性序和语义，带菱形的Horn公式的可满足性是不可判定的。相反，带盒Horn公式的可满足性在自反语义下对离散序和稠密序都是易处理的，在非自反语义下对稠密序都是易处理的，但在非自反语义下对离散序是不可判定的.在非自反语义下，具有方块和菱形的二元Horn公式的可满足性总是不可判定的。
2017-08-28 cs.CC cs.LO
Operational Semantics of Resolution and Productivity in Horn Clause Logic
本文研究了Horn子句逻辑中不同归结策略的运算性质和类型论性质。我们区分了四种不同的分辨率：统一分辨率（SLD分辨率），术语匹配分辨率，最近引入的结构分辨率和部分（或懒惰）分辨率。我们把它们统一表示为抽象的归约系统，这使我们能够对它们的性质进行彻底的比较分析。为了匹配这个小步骤的语义，我们建议霍华德的系统H作为一个类型理论的语义对应。使用系统H，我们将Horn公式解释为类型，并且将给定公式的推导解释为居住在公式给出的类型中的证明项。我们证明了这些抽象约简系统相对于系统H的可靠性，并证明了SLD-归结和结构归结相对于系统H的完备性。我们确定的条件下，结构分辨率在操作上相当于SLD分辨率。我们展示了没有存在变量的Horn子句程序的术语匹配解决方案与术语重写之间的对应关系。
2016-08-17 cs.LO
Expressibility at the machine level versus structure level: ESO universal Horn Logic and the class P
我们表明，ESO通用霍恩逻辑（存在的第二逻辑，其中第一阶部分是一个通用的霍恩公式）是不足以捕捉P，一类问题的决定在多项式时间。在输入词汇表中存在后继关系时，此语句为真。我们提供了两个证明-一个基于两个结构的约化积，另一个基于可逼近性理论（第二个证明是在假设P与NP不相同的情况下）。我们表明，这里的结果与Grädel（1991）中的结果之间的差异是由于本文处理的表达式是在“结构层面”，而Grädel（1991）中的表达式是在“机器层面”-一个比说的更容易的例子。
2012-07-23 cs.CC cs.LO
An abstract fixed-point theorem for Horn formula equations
TU Wien（维也纳工业大学）；University of Amsterdam（阿姆斯特丹大学）
针对计算机科学多应用中重要的Horn公式方程，本文在带最小不动点算子的一阶逻辑中证明了适用于抽象语义的抽象不动点定理，并阐述其在程序验证逻辑基础等计算逻辑领域的推论。
2025-11-11 cs.LO math.LO
Computing Horn Rewritings of Description Logics Ontologies
University of Oxford（牛津大学）
我们研究的问题重写本体O1表示在DL L1到本体O2在霍恩DL L2，使O1和O2是equisatifiable扩展时，与任意数据集。允许这种重写的本体服从于推理技术，以确保数据复杂性的易处理性。在L1扩展ALCF时显示不可判定性后，我们专注于设计有效的可检查条件，以确保霍恩重写的存在。通过提升现有的技术，将析取数据重写成普通数据的情况下，任意一阶程序与功能符号，我们确定了一类本体，承认霍恩重写多项式的大小。我们的实验表明，许多现实世界的本体满足我们的充分条件，从而承认多项式霍恩重写。
2015-04-21 cs.AI cs.LO
Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses
本文提出了一种基于规范自动转换的命令式程序正确性验证方法。给定一个程序prog，我们考虑形式为$\{φ\}$ prog $\{ψ\}$的部分正确性规范，其中断言$φ$和$ψ$是由可能递归的Horn子句的集合Spec定义的谓词，其前提中具有线性算术（LA）约束（也称为约束Horn子句）。验证方法包括在构造一组PC的约束Horn子句，其可满足性意味着$\{φ\}$ prog $\{ψ\}$是有效的。我们强调了一些限制的国家的最先进的约束霍恩子句求解方法，这里称为LA求解方法，证明可满足性的条款，通过寻找线性算术解释的谓词。特别是，我们证明了存在一些规格，不能证明有效的任何这些LA解决方法。这些规范要求证明一组包含非线性子句（即前提中有多个原子的子句）的受约束Horn子句的PC的可满足性。然后，我们提出了一个转换，称为线性化，PC转换成一组线性条款（即条款，在其前提中最多一个原子）。我们表明，几个规格，不能被证明是有效的LA解决方法，可以被证明是有效的线性化后。我们还提出了一种策略，用于执行线性化在一个自动的方式，我们报告的一些实验结果，通过使用我们的方法的初步实施。
2015-07-21 cs.LO cs.PL
(Quantified) Horn Constraint Solving for Program Verification and Synthesis
我们展示了如何自动工具的验证线性和分支的时间属性的程序，多线程，和功能的程序，以及程序合成可以自然地和统一地被视为求解器的约束条件的形式（量化）霍恩条款的背景逻辑理论。这样的观点可以提供各种优势，例如。例如，在一个实施例中，约束生成（也称为证明义务的生成）和约束求解（也称为证明发现）之间的关注点的逻辑分离、跨不同验证任务的求解器的重用、以及证明设计者从低级算法关注点中解放出来，反之亦然。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2014-05-29 cs.LO
Proceedings First Workshop on Horn Clauses for Verification and Synthesis
本卷包含HCVS 2014的会议记录，第一次Horn Clauses for Verification and Synthesis研讨会于2014年7月17日在奥地利维也纳举行，作为联邦逻辑会议（FLoC）的卫星活动和维也纳逻辑夏季（VSL 2014）的一部分。HCVS 2014隶属于第26届计算机辅助验证国际会议（CAV 2014）和第30届逻辑编程国际会议（ICLP 2014）。大多数感兴趣的程序验证和综合问题可以直接使用Horn子句建模，并且约束/逻辑编程和程序验证社区的许多最新进展都集中在有效地解决Horn子句提出的问题上。由于这些团体在不同的时期从不同的角度倡导关于核查和综合的Horn条款，因此举办HCVS研讨会是为了促进互动和富有成效的经验交流和整合。
2014-12-02 cs.LO cs.SE
SLD-Resolution Reduction of Second-Order Horn Fragments -- technical report --
我们提出了SLD-决议，不可判定的问题，找到一个有限的子集的一组条款，从整个集合可以得出使用SLD-决议的推导减少问题。我们研究了二阶Horn逻辑的各种片段的约简，并在归纳逻辑程序设计中有具体的应用。我们还讨论了如何将这些结果扩展到标准分辨率。
2019-02-26 cs.LO
Higher-Order Constrained Horn Clauses and Refinement Types
出于高阶函数程序自动验证中的应用，我们开发了一个概念的约束霍恩条款在高阶逻辑和决策问题，其可满足性。我们表明，虽然高阶子句的可满足系统一般不具有最小模型，有一个规范模型的概念，通过减少到一种单调逻辑程序的问题。在高阶程序验证的工作之后，我们开发了一个细化类型的系统，以推理和自动搜索模型。这为解决决策问题提供了一个合理但不完整的方法。最后，我们证明了一个扩展的决策问题，其中细化类型直接用作警卫存在量词可以减少到原来的问题。这个结果可以用来表明，高阶函数的性质，可定义使用细化类型也表示使用高阶约束霍恩子句。
2017-08-01 cs.LO cs.PL
On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic
二阶布尔逻辑是QBF的推广，其常数交替片段已知对于指数时间层次的水平是完全的。我们考虑这种逻辑的两种类型的限制：1）对项构造的限制，2）对布尔矩阵的形式的限制。对于第一类，我们考虑两种限制：首先，不允许嵌套使用适当的函数变量，其次规定每个函数变量必须以固定的参数序列出现。第二种，我们考虑霍恩，克罗姆，和核心片段的布尔矩阵。我们分类的复杂性的逻辑得到这两种类型的限制相结合。我们表明，在大多数情况下，逻辑与k交替块的函数量词是完整的指数时间层次的第k或（k-1）级。此外，我们建立NL-完全的克罗姆和核心片段，当k=1和第一类的限制都有效。
2020-07-08 cs.CC cs.LO
Horn Clauses in Hybrid-Dynamic First-Order Logic
我们提出了一个混合动态一阶逻辑作为一个正式的基础，可重构系统的指定和推理。顾名思义，我们开发的形式主义扩展了（多排序）一阶逻辑，具有混合逻辑和动态逻辑所共有的特征。这为处理可重构系统提供了某些关键优势，例如：（a）名词的签名，包括操作和关系符号，允许引用特定的可能世界/系统配置-如在混合逻辑的情况下;（b）刚性和柔性符号的区别签名，其中刚性符号在可能世界中被统一解释;这就支持了严格的量化形式，确保变量具有相同的解释，而不管在哪个可能的世界中对其进行评估;（c）混合术语，在严格的符号背景下增加逻辑的表达能力;以及（d）动态逻辑动作上的模态运算符，其被定义为二元名义关系上的正则表达式。然后，我们研究霍恩条款在这个混合动态逻辑，并开发了一系列的结果，导致一个初始语义定理的任意条款集。这表明混合动态一阶逻辑的一个重要片段具有良好的计算特性，可以作为定义可重构系统的可执行语言的基础。最后，我们列出了逻辑编程的基础，在这个片段证明了混合动力的变种Herbrand定理，减少了语义蕴涵的逻辑编程查询的程序搜索一个合适的答案替代。
2019-05-10 cs.LO
Existential Second Order Logic Expression With Horn First Order for Maximum Clique (Decision Version)
我们表明，最大团问题（决策版本）可以表示在存在二阶（ESO）逻辑，其中第一阶部分是一个霍恩公式在二阶量化谓词。在没有排序的情况下，一阶部分是$Π_2$ Horn;如果使用排序，则它是通用Horn（在这种情况下，二阶变量可以在多项式时间内确定）。更新：由于结果不正确，患者撤回。如果phi = phi_1 AND phi_2，并且phi是一个Horn公式，这并不意味着phi_1和phi_2都是Horn公式。此外，基数约束不能表示为ESO中的通用Horn语句（即使结构是有序的）。Graedel定理在较低的（机器）级别上是有效的，但在较高的级别上可能不是。
2010-10-02 cs.CC cs.LO math.LO
An encoding of array verification problems into array-free Horn clauses
自动验证程序的安全属性是困难的，如果程序作用于数组或其他形式的映射，则更难。存在许多方法来验证程序操作上的布尔和整数值（例如抽象的解释，反例引导的抽象细化使用插值），但转置它们数组属性已充满了困难。与大多数以前的方法相比，我们不引入一个新的抽象域或一个新的插值过程数组。相反，我们生成一个抽象的标量问题，并将其提供给一个预先存在的求解器，与可调precision.Our转换的问题表示使用霍恩条款，一个共同的格式与明确和明确的逻辑语义验证问题。我们的编码的一个重要特点是，它创建了一个非线性的霍恩问题，与树展开，即使下面的“平坦”的控制图结构通常会产生一个线性的霍恩问题，与线性展开。也就是说，我们的编码不能表示成另一个控制流图问题的编码，并真正利用霍恩子句格式的能力。我们说明了我们的方法与选择排序的功能正确性的完全自动化的证明。
2015-09-30 cs.LO cs.PL
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
本卷包含第三届程序等价和关系推理研讨会（PERR）和第六届验证与综合霍恩子句研讨会（HCVS）的联合后续会议记录，分别于4月6日和7日在捷克共和国布拉格举行，作为ETAPS的附属研讨会。
2019-07-08 cs.LO
Combining Forward and Backward Abstract Interpretation of Horn Clauses
前向分析和后向分析的交替是程序抽象解释中的一种标准技术，当我们希望证明某些不需要的程序状态不可达时，这种技术特别有用。当前用于组合Horn子句的前向（在逻辑编程术语中为自底向上）和后向（自顶向下）抽象解释的最先进技术是查询-应答转换。它转换了Horn子句系统，使得标准的前向分析可以从目标向前和向后传播约束。问答转换是有效的，但有我们希望解决的问题。为此，我们引入了一个新的后向收集语义，它适用于交替的前向和后向抽象解释的Horn子句。我们展示了如何交替可以用来证明无法达到的目标，以及如何每一个后续运行的分析产生一个完善的系统模型。实验上，我们观察到，结合向前和向后的分析是很重要的分析系统编码的问题，在C程序的可达性。特别是，遵循我们的新语义的组合提高了我们自己的抽象解释器的精度，包括与查询-答案转换系统的前向分析相比。
2017-08-07 cs.LO cs.PL
Removing Unnecessary Variables from Horn Clause Verification Conditions
验证条件（Verification Conditions，VC）是一种逻辑公式，其可满足性保证了程序的正确性。我们认为VC的形式约束霍恩条款（CHC），这是自动生成的编码（解释器）的程序设计语言的操作语义。VC是通过基于展开/折叠变换规则的程序专门化而得到的，并且正如在专门化解释器时经常发生的那样，它们包含不必要的变量，即，在验证下的程序的正确性证明不需要的变量。在本文中，我们适应的CHC设置的一些技术，开发用于删除不必要的变量，从逻辑程序，我们表明，在某些情况下，这些技术的应用增加了霍恩子句求解器的有效性时，证明程序的正确性。
2016-07-15 cs.LO cs.PL cs.SE
The Complexity and Expressive Power of Second-Order Extended Logic
本文研究二阶 Horn 逻辑族在有限结构上的表达力，证明 SO-HORN^r、SO-HORN*^r 与 FO(LFP) 等价且 SO-HORN* 为其真子逻辑，并借助 DATALOG 程序分层版本及 SO-EHORN^r 刻画 co-NP。
2022-09-11 cs.CC cs.LO
Collection analysis for Horn clause programs
我们考虑用数据结构包含的项的集合来近似它们。例如，列表，二叉树，元组等，可以近似为其中的项目的集合或多集合。这种近似可以用来提供逻辑程序的部分正确性。例如，人们可能希望指定，只要证明了原子$sort(t,s)$，则两个列表$t$和$s$包含相同的多项集（即，$s$是$t$的置换）。如果排序去除了重复项，则人们可能会推断$t$和$s$的基础项集合是相同的。如果这些结果可以静态和自动地确定，那么它们可能是有用的。我们提出了一个计划，这样的收集分析可以结构化和自动化。该方案的核心是使用线性逻辑作为Horn子句逻辑的计算逻辑。
2007-08-16 cs.LO
Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis
许多感兴趣的程序验证和综合问题可以直接使用Horn子句建模，CLP和CAV社区的许多最新进展都集中在有效地解决Horn子句提出的问题上。HCVS系列研讨会旨在汇集在约束/逻辑编程两个社区工作的研究人员（例如，ICLP和CP），程序验证（例如，CAV、TACAS和VMCAI）和自动演绎（例如，CADE，IJCAR），关于基于Horn子句的分析、验证和综合的主题。这些团体在不同的时期从不同的角度倡导关于核查和综合的霍恩条款，组织HCVS是为了促进互动和富有成效的经验交流和整合。
2018-09-12 cs.LO cs.PL cs.SE
Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic
逻辑编程（LP）是一种基于一阶Horn子句逻辑的程序设计语言，它使用SLD-归结作为半决策过程。有限的SLD计算是归纳的声音和完整的最少Herbrand模型的逻辑程序。对偶地，SLD分解的共递归方法将无限SLD计算视为连续逼近程序的最大完全Herbrand模型中包含的无限项。在LP中实现协递归的最新算法基于循环检测。然而，这样的算法只支持推理的逻辑蕴涵合理的条款，他们没有考虑到生产力的重要性质，在无限的SLD计算。因此，循环检测落后于交互式定理证明（ITP）和项重写系统（TRS）中的共归纳方法。结构分解是一种新提出的替代SLD分解的方法，它可以定义和半决定一个适合于LP的生产力概念。在本文中，我们证明了健全的结构分辨率相对于Herbrand模型语义生产归纳，共归纳，混合归纳共归纳逻辑程序。我们介绍了两个算法，支持共归纳证明搜索无限生产条件。一个算法结合了循环检测的方法与生产性结构的解决方案，从而保证生产力的共归纳证明的无穷有理项。另一种则允许对无限非理性生产性术语的片段进行懒惰的合理观察。这使得LP中的共归纳方法与ITP和TRS中基于生产力的共归纳观察方法相提并论。
2017-05-04 cs.LO
Reducing Higher-order Recursion Scheme Equivalence to Coinductive Higher-order Constrained Horn Clauses
高阶约束Horn子句（HoCHC）是高阶逻辑模理论的一个语义不变系统。HoCHC具有半判定背景理论上的半判定不可解性，适合于安全验证。关于它与更大类的高阶验证问题的关系，人们知之甚少。出于程序等价性的考虑，我们引入了一个共归纳版本的HoCHC，它具有最大的模型属性。我们将高阶递归方案（HoRS）的编码定义为HoCHC逻辑程序。这种编码的正确性降低了开放HoRS等价问题的可判定性-因此，LambdaY-演算Böhm树等价问题-在一个完整的可判定树理论上的共归纳HoCHC的半可判定性。
2021-09-10 cs.FL cs.LO cs.PL
Coinductive Uniform Proofs
共归纳在霍恩子句逻辑中有两种形式：循环性质和关系的证明，以及涉及无限数据构造的证明。这两种共归纳推理的证明都曾在文献中出现过，但缺乏对这两种证明及其关系的系统分析。我们提出了一个一般的证明理论框架，处理这两种共同归纳霍恩子句逻辑。为此，我们提出了一个共同归纳的Miller等人的框架的统一证明，并证明其可靠性相对于共同归纳模型的霍恩子句逻辑。
2019-03-18 cs.LO
A Fragment of Dependence Logic Capturing Polynomial Time
本文研究了Horn公式在依赖逻辑中的表达能力，证明了Horn公式可以表达NP完全问题。因此，我们定义了一个更小的片段D-Horn*，并表明，在有限的后继结构，它捕获的复杂性类P的所有集可判定的多项式时间。进一步研究了我们的结果是否可以推广到D-Horn* 的开公式和所谓的向下单调多项式时间性质的情形。
2014-09-03 cs.CC cs.LO
Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation
这些会议记录包括在第九届验证和合成霍恩条款研讨会和第十届验证和程序转换国际研讨会上提交的选定论文，这两个研讨会都隶属于ETAPS 2022。许多感兴趣的程序验证和综合问题可以直接使用Horn子句建模，CLP和CAV社区的许多最新进展都集中在有效地解决Horn子句提出的问题上。HCVS系列研讨会旨在汇集在约束/逻辑编程社区工作的研究人员（例如，ICLP和CP），程序验证（例如，CAV、TACAS和VMCAI）和自动演绎（例如，CADE，IJCAR），关于基于Horn子句的分析、验证和综合的主题。这些团体在不同的时期从不同的角度倡导关于核查和综合的霍恩条款，组织HCVS是为了促进互动和富有成效的经验交流和整合。VPT研讨会的目的是汇集在程序验证和程序转换领域工作的研究人员。这两个领域之间有很大的潜力进行有益的互动，因为：1）一方面，在程序转换领域开发的方法和工具，如部分评估，折叠/展开转换和超级编译，都已成功应用于验证无限状态和参数化系统。2)另一方面，模型检验，抽象解释，SAT和SMT解决和自动定理证明已被用来加强程序转换技术。此外，程序转换工具的正式认证，如自动重构工具和编译器，最近吸引了相当大的兴趣，提出了重大挑战。
2022-11-19 cs.LO cs.PL cs.SC
Expressivity of Planning with Horn Description Logic Ontologies (Technical Report)
Saarland University（萨尔大学）；University of Freiburg（弗莱堡大学）
人工智能规划中的状态约束在全球范围内限制了法律环境状态。标准规划语言做出封闭域和封闭世界的假设。在这里，我们解决开放世界的状态约束正式规划的描述逻辑（DL）本体。以前，这种DL和规划的结合已经被研究用于轻型DL DL-Lite。在这里，我们提出了一种新的编译方案，标准PDDL派生谓词，这适用于更有表现力的DL和基于DL查询到数据库的可重写性与分层否定。我们还提供了一个新的可重写性结果的DL霍恩ALCHOIQ，这使我们能够将我们的编译方案相当表达的本体。相比之下，我们表明，在轻微的扩展角SROIQ没有这样的编译是可能的，除非弱指数层次崩溃。最后，我们表明，我们的方法可以优于以前的工作，现有的基准规划与DL本体，是可行的新基准利用更具表现力的本体。这是AAAI 22接受的论文的扩展版本。
2022-03-17 cs.AI cs.CC cs.LO
Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis
会议记录包括阿尔贝托的主题论文，随后由洛伦佐克莱门特（美国）撰写的6份邀请论文。华沙），阿兰芬克尔（美国。Paris-Saclay），John Gallagher（Roskilde U.和IMDEA软件研究所）等，尼尔·琼斯（美国）Copenhagen）等人，Michael Leuschel（Heinrich-Heine U.）和Maurizio Proietti（IASI-CNR）等人。这些邀请论文之后是VPT 2020上接受的4篇常规论文和HCVS 2020的论文，其中包括三篇投稿论文和一篇关于第三届约束Horn子句求解器竞赛的邀请论文。此外，Andrzej Skowron（U.华沙），索菲雷诺（EPO）和莫阿约翰逊（查尔默斯大学），包括在内。
2020-08-06 cs.LO cs.PL cs.SC
Horn-ICE Learning for Synthesizing Invariants and Contracts
Indian Institute of Science（印度科学学院）；Amazon India（亚马逊印度）；University of Illinois, Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）
我们设计了学习算法合成不变量使用霍恩蕴涵反例（霍恩ICE），扩展ICE学习模型。特别是，我们描述了一个决策树学习算法，学习霍恩ICE样本，工作在多项式时间，并使用统计算法来学习小树，满足样本。由于大多数验证证明可以使用Horn子句建模，Horn-ICE学习是一种更强大的技术，可以学习证明程序正确的归纳注释。我们的实验表明，我们的算法的实现是能够学习足够的归纳不变量和合同有效地为各种顺序和并发程序。
2017-12-26 cs.LG cs.LO cs.PL
The Relationship between Craig Interpolation and Recursion-Free Horn Clauses
尽管经过数十年的研究，软件程序中仍然有许多常见的概念被认为对验证具有挑战性：其中包括并发性以及程序与过程的组合分析。作为一个有前途的方向，以克服这些困难，最近使用的Horn约束作为软件程序的中间表示已被提出。Horn约束与Craig插值有关，Craig插值是用于在验证中构造和细化抽象以及合成归纳循环不变量的主要技术之一。我们给出了一个调查的不同形式的克雷格插值在文献中发现，并表明，它们都对应于自然片段（递归自由）霍恩约束。我们还讨论了解决递归自由霍恩约束系统的技术。
2013-02-18 cs.LO
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
我们提出了一个组合SMT为基础的算法的安全程序，考虑到堆以及。现有的基于SMT的方法要么在很大程度上限于处理线性算术运算和属性，或者是非组合的。我们使用约束角子句（CHCs）来表示验证条件，其中使用阵列的扩展理论（ARR）的内存操作建模。首先，我们描述了一个指数时间量词消去（QE）算法的ARR，它可以引入新的量词的索引和值排序。其次，我们适应QE算法，以有效地获得下近似使用模型，从而在多项式时间基于模型的投影（MBP）算法。第三，我们集成的MBP算法的框架中的组合推理的过程性程序使用的可能和必须的摘要，我们最近提出的。我们对CHC的解决方案目前仅限于无量词公式。最后，我们描述了我们的实践经验，在SV-COMP'15基准测试中使用的工具SPACER的实现。
2015-08-06 cs.LO cs.PL cs.SE
A First Polynomial Non-Clausal Class in Many-Valued Logic
Artificial Intelligence Research Institute (IIIA) - CSIC（人工智能研究所 (IIIA) - CSIC）
多项式公式类与演绎效率的相关性激发了他们的搜索，目前，已知有大量这样的类。尽管如此，它们一直专门在小句形式和命题逻辑的设置中寻找，这当然对实际应用有明显的限制。因此，最近提出了第一个非子句（NC）形式的多项式命题类。沿着这些路线，并朝着NC易处理性适用于超越命题逻辑，首先，我们定义了正规多值霍恩非子句类，或RH，通过适当合并两个正规类：霍恩和NC。其次，我们证明了（1）RH与正则Horn类之间的关系是：在句法上RH包含Horn类，但两者在语义上是等价的;（2）RH与正则非小句类之间的关系是：RH包含所有小句形式为Horn的NC公式。第三，我们定义了正则非子句单位归结，或RUR-NC，并证明了它是RH的完全的，并在多项式时间内检查其可满足性。后一个事实表明，由于RH是多值的，非子句的和易处理的，我们的预期目标已经达到。由于RH和RUR-NC都是DPLL方案的基础，在命题逻辑中是最有效的，并且可以扩展到其他一些非经典逻辑，我们认为它们为基于DPLL的高效非子句近似推理铺平了道路。
2021-10-21 cs.AI cs.LO
Belief merging within fragments of propositional logic
Aix Marseille Université（艾克斯-马赛大学）；CNRS（法国国家科学研究中心）；Vienna University of Technology（维也纳工业大学）
最近，在命题逻辑片段的框架内的信念变化得到了越来越多的关注。以往的研究主要集中在Horn片段上的信念收缩和信念修正。然而，在命题逻辑的片段的信念合并的问题一直被忽视。本文提出了一种通用的方法来定义新的合并运算符来自现有的，这样的合并结果仍然在考虑中的片段。我们的方法不仅限于霍恩片段的情况下，但适用于任何片段的命题逻辑的特点是封闭属性的模型集的公式。我们研究的逻辑属性的建议运营商的合并假设的满意度，特别考虑到基于距离的合并运营商的霍恩和克罗姆片段。
2014-04-25 cs.AI cs.LO
Symbolic Execution of Constrained Horn Clauses
TU Vienna（维也纳工业大学）；Uppsala University（乌普萨拉大学）；University of Regensburg（雷根斯堡大学）
本文研究约束 Horn 子句的符号执行，提出约束消解演算，统一前向与后向推理，证明完备性并开发剪枝准则，实验验证于 Eldarica 求解器。
2026-10-05 cs.LO cs.PL
Contract Strengthening through Constrained Horn Clause Verification
一个程序的函数属性通常通过为它的每个函数提供一个契约来指定。一个函数的契约由一对公式组成，称为前置条件和后置条件，它们分别在该函数执行之前和之后保持有效。可能的情况是，程序员提供的契约不足以允许验证系统证明程序的正确性，也就是说，对于每个函数，如果前置条件成立，并且函数的执行终止，则后置条件成立。我们解决这个问题，通过提供一种技术，可以加强后置条件的功能，从而提高验证程序的正确性的能力。我们的技术包括四个步骤。首先，翻译的给定程序，它可以操纵代数数据结构（ADT），其合同成一组受约束的霍恩条款（CHC）的可满足性意味着给定的合同的有效性。然后，通过由VeriCaT工具执行的CHC转换，导出一组新的CHC，这些CHC仅操作基本排序（例如布尔或整数），并且其可满足性暗示了原始子句集的可满足性。然后，使用CHC求解器SPACER为基本排序构造新的派生CHC的模型（如果有的话）。最后，将该模型转化为适当加强给定合同的后置条件的公式。我们将通过一个由Scala程序组成的用于反转列表的示例来展示我们的技术。请注意，当考虑给定的合同时，Stainless验证器无法证明该程序的正确性，而当考虑通过应用我们的技术构造的具有增强后条件的合同时，它成功了。
2022-11-22 cs.LO cs.PL
Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
程序性质的证明可以归结为一组约束Horn子句（CHC）的可满足性证明，这些约束Horn子句可以由程序和程序性质自动生成。在本文中，我们已经进行了一个案例研究，在霍恩子句验证，考虑几个排序程序的转换技术，使我们能够消除归纳数据结构，如列表或树的有效性进行了探索。如果这种技术是成功的，我们得到一组CHC的整数和布尔值的约束，可满足性检查通常可以通过使用最先进的CHC求解器，如Eldarica或Z3，以有效的方式进行。在这个案例研究中，我们还说明了一个配套技术的有用性的基础上引入所谓的差异谓词，其定义对应于在验证过程中所需的引理。我们已经考虑了实现以下类型的排序算法作用于整数列表的函数程序：（i）线性递归排序算法，如插入排序和选择排序，以及（ii）非线性递归排序算法，如快速排序和合并排序，我们已经考虑了以下性质：（i）部分正确性属性，即输出列表的有序性，以及当被视为多集时输入和输出列表的相等性，以及（ii）一些算术属性，例如排序之前和之后的元素之和相等。
2019-07-09 cs.LO cs.PL cs.SC
On Sub-Propositional Fragments of Modal Logic
本文研究模态逻辑 K、T、K4 和 S4 的亚命题片段（如 Horn、Krom 等）的表达能力层级，并证明无菱形的 Horn 片段可满足性问题是多项式时间可解的。
2018-06-21 cs.LO
Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
我们解决的问题，验证程序的功能满足他们的合同，指定的前/后条件。我们遵循一种基于约束Horn子句（CHCs）的方法，通过该方法，验证问题被简化为检查来自给定程序和合同的一组子句的可满足性的问题。我们认为程序，操作代数数据类型（ADT）和一类合同指定的蜕变，即简单的递归模式定义的给定ADT的功能。我们通过几个例子表明，国家的最先进的CHC可满足性工具是不能有效地解决可满足性问题的合同直接翻译成CHCs。为了克服这个困难，我们提出了一种转换技术，删除ADT条款的CHCs和派生新的条款，工作在基本排序，如整数和布尔。因此，当使用衍生的CHC时，不需要关于ADT的归纳规则。我们证明了变换是合理的，也就是说，如果CHCs的导出集是可满足的，那么原来的集合也是可满足的。我们还证明了转换总是终止的合同指定的类的蜕变。最后，我们提出了我们的技术的实现时，验证许多非平凡的合同ADT操纵程序所获得的实验结果。
2022-09-07 cs.LO cs.PL
CTL* Verification and Synthesis using Existential Horn Clauses
Technion - Israel Institute of Technology（以色列理工学院）
本文提出基于存在性Horn子句（EHCs）的自动验证与合成方法，用于无限状态反应程序对CTL*规格的验证，展示了其在复杂系统中的应用。
2024-08-21 cs.LO
CoALP-Ty'16
本卷构成了研讨会上的预诉讼程序，霍恩子句逻辑编程和类型（CoALP-Ty'16），在爱丁堡举行的28- 29十一月2016作为EPSRC格兰特Coalgebraic逻辑编程类型推断结束的标志，由E。Komendantskaya和J. Power.本卷包括扩展摘要描述当前的研究在以下领域：语义：Lawvere理论和余代数在逻辑和函数式编程程序设计语言：霍恩子句逻辑类型推断在函数式语言和超越讨论后，在研讨会上的作者的扩展摘要将被邀请提交一份完整的文件，通过第二轮的裁判和选择的正式程序。
2016-12-09 cs.LO
Efficient CTL Verification via Horn Constraints Solving
时态逻辑的使用一直被认为是反应式系统的形式化规范和验证的基本方法。在本文中，我们采取的问题，自动验证的时间属性，由CTL公式，为一个给定的（可能是无限状态）的程序。我们提出了一种方法的基础上编码的问题作为一组霍恩约束。该方法以一个程序，建模为一个过渡系统，并作为输入的CTL公式给出的属性。首先利用CTL公式的句法结构生成一组普遍存在的量化Horn约束和良基约束。然后，通过应用现成的Horn约束求解引擎来求解生成的约束集。当且仅当生成的约束集有解时，程序才满足该性质。我们证明了实际的承诺的方法，通过将其应用于一组具有挑战性的例子。虽然我们的方法是基于一个通用的霍恩约束求解引擎，它是能够超越国家的最先进的方法专门为CTL验证。
2016-07-15 cs.LO
Lower Bounds on Syntactic Logic Expressions for Optimization Problems and Duality using Lagrangian Dual to characterize optimality conditions
我们表明，简单的语法表达式，如存在二阶（ESO）通用霍恩公式可以表示NP-难优化问题。决策问题和优化问题的表达方式有很大的不同。这类似于两类问题的计算时间差异;例如，2SAT Horn公式可以在多项式时间内满足，而优化版本则是NP难的。已知所有多项式可解的决策问题在后继关系存在的情况下都可以表示为ESO泛（$Π_1$）Horn语句。我们在这里表明，另一方面，如果$P \neq NP$，优化问题无视这样的特征，通过证明，即使是$Π_0$（量词免费）霍恩公式是无法保证多项式时间可解性。最后，通过连接的概念，在优化对偶与描述的复杂性，我们将展示一种方法，通过该方法，优化问题可以解决一个单一的调用“决策”图灵机，而不是多个调用使用经典的二分搜索设置。
2011-07-24 cs.CC cs.LO
From Big-Step to Small-Step Semantics and Back with Interpreter Specialisation
我们调查表示的强制性程序作为约束霍恩条款。从操作语义转换规则开始，我们着手编写解释器作为受约束的霍恩子句程序直接编码的规则。然后，我们专门一个解释器相对于一个给定的源程序，以实现编译的源语言霍恩条款（第一个二村投影的实例）。该过程是详细描述了一个解释器的一个子集的C语言，直接编码的大步骤操作语义的规则。类似的翻译基于小步语义可以进行，但我们展示了一种方法来获得一个小步表示使用线性解释器大步霍恩条款。该解释器再次专门用于实现从大步到小步风格的翻译。使用第三个解释器可以将线性小步程序转换回大步非线性程序。使用Tarjan算法计算线性规划的正则路径表达式，然后该正则表达式引导解释器计算程序路径。在所有的转换阶段，我们使用一个既定的部分评估器和利用标准的逻辑程序转换，以消除冗余的数据结构和参数的谓词和重命名的谓词，以明确其链接到原始源程序中的语句。
2020-08-07 cs.LO cs.PL cs.SC
A Theory of Heap for Constrained Horn Clauses (Extended Technical Report)
约束Horn子句（CHC）是一种中间程序表示，可以由几个验证工具生成，并且可以由许多Horn求解器处理和求解。在验证中使用CHC时的主要挑战之一是堆分配的数据结构的编码：这种数据结构今天要么使用数组理论显式表示，要么在不变量或细化类型的帮助下转换，击败CHC作为语言独立的表示以及Horn求解器实现的算法的不可知性。本文提出了一种适用于CHC的SMT-LIB堆理论，目的是为具有堆数据结构的程序提供一种标准的交换格式。我们介绍了堆理论的语法，定义其语义的公理和使用减少SMT-LIB数组和数据类型，并讨论其属性和大纲可能的扩展和未来的工作。
2021-04-09 cs.LO
The (Lazy) Functional Side of Logic Programming
将逻辑程序转换成功能程序的可能性一直是研究的课题。许多方法的共同点是，原始逻辑程序，为了被翻译，需要被良好地模态化，这导致了这样的共识，即这些程序可以被认为是逻辑程序的“功能部分”。因此，“复杂”逻辑变量、动态选择规则的可能性以及非良模程序的一般属性是逻辑程序的独有特征，这一点已被广泛接受。这并不完全正确，因为其中一些特性在惰性函数式语言中自然存在。我们通过定义一个适用于更广泛的逻辑程序的简单翻译，重新讨论了什么功能是逻辑编程范式所独有的老问题，并证明了目前的界限是不合理的限制。
2000-03-20 cs.LO cs.PL
Algebraic Semantics of Datalog with Equality
讨论了关系Horn逻辑（RHL）和部分Horn逻辑（PHL）的语法和语义. RHL是Datasheet程序设计语言的扩展，它允许在结论中引入和等同变量。PHL是RHL通过部分函数的句法扩展，并且是本质代数理论的许多等价概念之一。我们的主要贡献是构建了一个新的自由模型。我们关联到RHL和PHL序列分类态射，这使我们能够使用提升特性来表征逻辑满意度。然后，我们得到自由和弱自由模型使用小对象参数。小对象参数可以被理解为Datasheet评估的抽象概括。它支持Eqlog Datlog引擎的实现，该引擎计算PHL理论的自由模型。
2023-02-22 cs.LO
Combining Logic Programs and Monadic Second Order Logics by Program Transformation
本文提出了一种基于展开/折叠变换规则的程序合成方法，该方法可用于从一个后继者的弱一元二阶理论（WS 1 S）的公式导出可终止的确定性逻辑程序。这种综合方法也可作为WS_（1 S）封闭公式的判定过程的证明方法。我们应用我们的综合方法翻译CLP（WS 1 S）程序到逻辑程序，我们也使用它作为一种证明方法来验证无限状态系统的安全性。
2003-11-27 cs.LO cs.PL
An iterative approach to precondition inference using constrained Horn clauses
我们提出了一种方法，用于自动推理的条件上的初始状态的程序，保证在程序中的安全断言不被违反。约束霍恩条款（CHCs）被用来建模的程序和断言在一个统一的方式，我们使用标准的抽象解释，得出一个过度近似的不安全的初始状态。前提条件则是对应于该集合的补集的约束，欠近似安全初始状态的集合。这种互补的想法并不新鲜，但以前试图利用它的尝试已经失去了精确性。在这里，我们开发了一种迭代专门化算法，以提供更精确的，在某些情况下最佳的安全条件。该算法结合了现有的转换，即约束专业化，部分评估和消除痕迹的转换。这些转换中的最后两个执行多变量专门化，从而导致提高精度的析取约束。该算法的实现和测试的基准套件的程序从文献中的前提推理和软件验证比赛。
2018-04-17 cs.LO
Automated Termination Analysis for Logic Programs with Cut
可终止性是逻辑程序的一个重要性质，也是研究得很好的性质。然而，几乎所有的自动终止分析方法都集中在确定的逻辑程序上，而实际的Prolog程序通常使用cut运算符。本文介绍了一种新的预处理方法，它能自动地将Prolog程序转换成无割的逻辑程序，其中无割程序的终止意味着原程序的终止。因此，在该预处理之后，可以应用用于证明确定逻辑程序的终止的任何技术。我们在我们的终止证明程序AProVE中实现了这种预处理，并成功地进行了广泛的实验。
2010-07-28 cs.LO cs.PL
Nested Sequents for Horn-Characterizable Quantified Modal Logics with Equality via Reachability Rules
Technische Universität Dresden（德累斯顿工业大学）；University of Bologna（博洛尼亚大学）
本文提出了一种无割的嵌套序列系统，用于处理具有内外域的量模态逻辑，通过可达规则实现域条件的自然定义，并证明了系统的完备性和证明论性质。
2026-04-20 cs.LO math.LO
Verification of Programs by Combining Iterated Specialization with Interpolation
我们提出了一个程序安全的验证技术，结合迭代专业化和插值霍恩子句求解。我们的新方法组合在一起，这两种技术在一个模块化的方式，利用共同的霍恩子句表示的验证问题。迭代专业化验证器通过使用展开/折叠等价保持转换规则来转换验证条件的初始集合。在转换过程中，程序不变量是通过应用加宽运算符来发现的。然后通过插值霍恩子句求解器分析专用验证条件的输出集，从而将插值的效果添加到加宽的效果中。特殊化和插值阶段可以迭代，也可以与其他改变约束传播方向的转换（从程序前提条件向前或从错误条件向后）相结合。我们已经实现了我们的验证技术集成VeriMAP验证器与FTCLP霍恩条款求解器，迭代专业化和插值的基础上，分别。我们的实验结果表明，集成验证器提高了每个单独运行的组件的精度。
2014-12-03 cs.LO cs.SE
The Logic of Logic Programming
本文主张逻辑编程的本质是归纳定义逻辑而非经典逻辑的 Horn 子句子逻辑，并以此解释 Prolog 程序与数学归纳定义的根本相似性，为相关语义问题提供自然解答。
2023-04-26 cs.LO
