Defeasible Modalities
非单调逻辑的特征通常是存在一些“条件”的概念,而这些概念不具有单调性。因此,对非单调逻辑的研究主要关注的是论证形式的可废止性及其组成部分的相关正规性(或反常性)。相反,可废止的推理模式旨在形式化模态概念的可废止方面,如行动,义务和知识。在这项工作中,我们丰富了标准的可能世界语义与世界上的Kripke模型的偏好排序。由此产生的模态逻辑家族允许可废止模态的优雅表达。我们还提出了一个表演算,这是健全的和完整的关于我们的优惠语义。
2013-10-23 cs.LO
Nonmonotonic Logics and Semantics
塔斯基给出了演绎推理的一般语义:一个公式a可以从一组公式A中推导出来,当且仅当a在所有模型中成立,其中A的每个元素都成立。一个更自由的语义被认为是:公式a可以从一组公式A中推导出来,当且仅当a在所有的“偏好”模型中成立,其中A的所有元素都成立。Shoham提出“首选”模型的概念可以通过底层语言模型的部分排序来定义。本文描述了一个更一般的语义,基于一组自然属性的选择功能。这种语义在这里被证明是等价于语义的基础上比较的相对“重要性”的模型集,由什么金额的定性概率测量。等价语义定义的结果操作的特点,然后由Tarski的性质,其中的单调性要求被替换为三个较弱的条件的削弱。经典命题连接词在非单调环境下具有自然的引入-消去规则。即使在非单调的设置,人们获得经典的命题逻辑,从而表明单调性是不需要证明经典的命题连接词。
2002-04-15 cs.AI cs.LO math.LO
Post-Proceedings of the First International Workshop on Learning and Nonmonotonic Reasoning
知识表示与推理和机器学习是人工智能的两个重要领域。非单调逻辑程序设计(NMLP)和回答集程序设计(ASP)为常识知识的表示和推理提供了形式语言,实现了人工智能中的声明式问题求解。另一方面,归纳逻辑程序设计(ILP)在逻辑程序设计中实现了机器学习,为归纳学习提供了形式化的背景,并将其应用于关系学习和数据采掘等领域。一般来说,NMLP和ASP实现了非单调推理,但缺乏学习能力。相反,ILP实现了归纳学习,而大多数技术都是在经典单调逻辑下发展起来的。在这种背景下,一些研究者试图将各种技术结合到非单调ILP中。这样的组合将引入一个学习机制的程序,并将利用新的应用程序的NMLP侧,而在ILP侧,它将扩展的表示语言,使我们能够使用现有的求解器。学习和非单调推理之间的交叉也可以发生在诸如使用答案集求解器用于ILP、在运行答案集求解器时加速学习、学习动作理论、学习动力系统中的转换规则、溯因学习、学习具有抑制的生物网络以及涉及默认和否定的应用中。该研讨会是首次尝试提供一个公开论坛,以确定问题和讨论具有互补专长的研究人员之间可能的合作。该研讨会于2013年9月15日在西班牙Corunna举行。这篇论文集包含五篇技术论文(六篇被接受的论文中的五篇)和Luc De Raedt邀请演讲的摘要。
2013-11-19 cs.AI cs.LG cs.LO
Characterization of Strongly Equivalent Logic Programs in Intermediate Logics
与逻辑程序的答案集语义相关的非经典、非单调推理关系产生了逻辑程序之间的“强等价”关系,该关系可以在3值Goedel逻辑G3中得到验证,G3是最强的非经典中间命题逻辑(Lifschitz,Pearce和Valverde,2001)。本文将证明KC(通过将公理~A v ~A加到直觉逻辑中而得到的逻辑)是最弱的中间逻辑,对于它,强等价的逻辑程序在允许否定的语言中是逻辑等价的。
2002-06-03 cs.LO
Implementing Default and Autoepistemic Logics via the Logic of GK
University of Science and Technology of China(中国科学技术大学);Leipzig University(莱比锡大学)
知识和合理假设的逻辑,也称为基础知识逻辑(GK),由林和肖汉姆提出,作为非单调推理的一般逻辑。到目前为止,它已经被用来嵌入默认逻辑(命题情况),自认知逻辑,特纳的普遍因果关系逻辑,以及稳定模型语义下的一般逻辑编程。除了显示GK作为非单调推理逻辑的一般性之外,这些嵌入还揭示了这些其他逻辑之间的关系。在本文中,第一次,我们展示了如何GK的逻辑可以嵌入到析取逻辑编程中的多项式,但非模块化的新变量的翻译。其结果可用于计算缺省逻辑、自认知逻辑和Turner泛因逻辑的扩展/扩展语义,并可通过claspD(-2)、DLV、GNT和cmodels等析取ASP求解器进行求解。
2014-05-05 cs.AI cs.LO
Towards Constraint Temporal Answer Set Programming
University of Corunna, Spain;University of Angers, France;CRIL CNRS \& Artois University, France;University of Potsdam, Germany
本文提出了一种结合时间逻辑和约束的ASP扩展,用于实现高精度动态系统推理。
2025-07-18 cs.AI cs.LO
Axiomatic Aspects of Default Inference
本文从基于语义的角度研究了非单调结果公理,重点研究了一类不需要预定义语法/逻辑就可以进行部分信息推理的数学结构。这种结构称为默认结构。我们研究公理的非单调后果关系来自扩展赖特的默认逻辑,使用怀疑推理,但扩展现在用于建设可能的世界在一个默认的信息结构。在以前的工作中,我们表明,怀疑推理所产生的默认扩展遵守一套良好的公理,包括谨慎削减公理。我们在这里表明,值得注意的是,反过来也是正确的:任何遵循这套公理的后果关系可以表示为一个从怀疑推理构建。我们给出了非单调后果关系的公理和扩张性质的表示定理,并给出了满足谨慎单调律的非单调系统与具有唯一扩张的缺省结构之间的一一对应关系.我们的研究结果给出了一组管理更新的非单调知识库的基本规则的理论依据,证明了它们的派生更具体和原始的建设的扩展。同样引人注目的是,表示定理的证明表明,只有浅扩展是必要的,在这个意义上,实现扩展所需的迭代次数最多为三次。所有这些发展都是通过采取更自由的一致性观点而实现的:一致性是用户定义的谓词,满足一些基本属性。
2002-07-25 cs.LO
Logic Programming, Functional Programming, and Inductive Definitions
报告了统一逻辑和函数式编程的尝试。作为出发点,我们认为“逻辑程序“不是关于逻辑的,而是构成集合和关系的归纳定义。基于这些考虑的骨架语言设计的草图和原型实现进行了讨论。
2001-03-29 cs.LO
The Logic of Logic Programming
本文主张逻辑编程的本质是归纳定义逻辑而非经典逻辑的 Horn 子句子逻辑,并以此解释 Prolog 程序与数学归纳定义的根本相似性,为相关语义问题提供自然解答。
2023-04-26 cs.LO
A Tractable Logic for Molecular Biology
我们介绍了一个逻辑的知识表示和推理的蛋白质-蛋白质相互作用。模理论,公式描述蛋白质结构和动态变化。它们可以组合以添加或删除静态和动态观测。一个二阶外切算子,然后使非单调推理的公式所隐含的变化。我们引入演绎规则,产生的公式,等价,在一阶片段与可判定的可满足性和有效性。重要的是,规则可以产生外接公式。
2019-09-18 cs.LO
Incorporating Inductions and Game Semantics into Logic Programming
归纳和博弈语义是对传统逻辑程序设计的两个有用的扩展。具体地说,归纳法可以捕获逻辑编程中更广泛的一类可证明公式。采用博弈语义可以使逻辑编程更具交互性。在本文中,我们提出了一个执行模型的逻辑语言与这些功能。这种执行模型密切遵循现实生活中的推理过程。
2015-08-08 cs.LO
Structural Resolution for Logic Programming
我们介绍了一个三层树演算(3 TC),定义了一个系统的方式,在逻辑编程中的证明搜索的三层树结构。我们使用3 TC来定义一个新的-结构化-版本的解决逻辑编程。
2015-07-21 cs.LO
The Complexity of Circumscription in DLs
University of Naples Federico II(那不勒斯费德里科二世大学);University of Bremen(不来梅大学);University of Liverpool(利物浦大学)
作为一阶逻辑的一部分,描述逻辑不具有可废止继承和缺省规则等非单调特性。由于许多应用程序将受益于这些功能的可用性,已经开发了几个家庭的非单调DL,主要是基于默认逻辑和自认知逻辑。在本文中,我们认为限制作为一个有趣的替代方法,非单调的DL,特别是,支持可废止的继承在一个自然的方式。我们研究了在不同的语言限制和不同的约束条件下扩展的DLs的最小化,固定和变化的谓词集,并查明确切的计算复杂性的推理DLs范围从ALC ALCIO和ALCQO。当最小化谓词和固定谓词只包括概念名称但不包括角色名称时,则NExpTime^NP的推理完成。对于NP^NExpTime,当最小化谓词和固定谓词的数量由一个常数限制时,它就成为完备的。如果角色可以被最小化或固定,那么复杂性范围从NExpTime^NP到不可判定性。
2014-01-15 cs.AI cs.LO
Binary Non-Termination in Term Rewriting and Logic Programming
该研究提出一种新的句法准则,可在包含简化项重写与逻辑编程的抽象场景中实现非终止性的自动检测。
2023-07-21 cs.LO
Logic Programming with Default, Weak and Strict Negations
本文讨论了逻辑程序设计中的三种否定:缺省否定、弱否定和严格否定。讨论了具有三种否定的逻辑程序的三值逻辑模型理论。该过程是为否定而构造的,因此,根据三值逻辑模型理论,该过程是可靠的。
2005-11-10 cs.LO
Combining Fixed-Point Definitions and Game Semantics in Logic Programming
具有定点定义的逻辑程序设计是传统逻辑程序设计的一个有用的扩展。固定点定义可以捕获简单的模型检验问题和封闭世界假设。它的操作语义通常基于直觉可证明性。我们扩展了这些语言的操作语义与游戏语义。这种扩展的语义有几个有趣的方面:特别是,它为$read$谓词提供了逻辑状态。
2015-08-05 cs.LO
Coalgebraic Semantics for Probabilistic Logic Programming
本文提出概率逻辑编程的余代数语义,通过函子F的余代数建模程序,并利用余自由余代数给出推导树与可能世界两种语义,可恢复分布语义,并扩展至加权逻辑编程。
2021-04-09 cs.LO
Category theoretic semantics for theorem proving in logic programming: embracing the laxness
命题逻辑程序$P$可以用程序中的原子命题集合上的$P_fP_f$ -余代数来标识。相应的$C(P_fP_f)$ -余代数,其中$C(P_fP_f)$是$P_fP_f$上的余自由余代数,描述了归结导子.使用宽松的语义,这种对应关系可以扩展到一类没有存在变量的一阶逻辑程序。由此产生的扩展捕获逻辑编程中的术语匹配分辨率的证明。完善宽松的方法,我们进一步扩展到任意逻辑程序。我们还展示了一个完善的Bonchi和Zanasi的饱和语义逻辑编程,补充宽松的语义。
2016-02-17 cs.LO
Default reasoning over domains and concept hierarchies
W.C.圆和G。- Q. Zhang(2001)提出研究一种推广到代数域的析取逻辑编程形式。该系统允许推理的信息是分层结构,并形成一个(合适的)域。我们扩展这个框架,包括推理与默认否定,从而产生一个新的非单调推理框架的层次知识,其中包括答案集编程与扩展的析取逻辑程序。我们还表明,层次结构的知识,编程在这种模式下可以做的,产生非常自然的正式概念分析。总之,我们得到了一个默认的推理范式的概念知识,这是根据非单调推理的主流发展。
2004-09-01 cs.AI cs.LO
Program Logics for Homogeneous Generative Run-Time Meta-Programming
本文提供了同构生成运行时间元编程的第一个程序逻辑-使用Davies和Pfenning的MiniML变体作为其底层Meta程序设计语言。我们证明了我们的方法的适用性推理的例子元程序从文献。我们还证明了我们的逻辑是相对完整的库克意义上,使归纳推导的特征公式,并准确地捕捉观察属性诱导的操作语义。
2017-03-29 cs.LO
Programming in logic without Prolog
逻辑可以独立于逻辑编程而用于编程和数据库。为了在这方面发挥作用,逻辑必须提供一种机制,以便根据在解释逻辑理论时所给出的那些函数和关系来定义新的函数和关系。我们通过在经典语义之上创建组合语义来提供这种机制。在这种方法中,计算结果的验证依赖于逻辑解释与Java或C++等语言中的类定义之间的对应关系。这种方法的优点是结合了程序员的表达媒介,在C++的情况下,优化使用计算机资源。
2014-12-27 cs.LO
Approximation Fixpoint Theory as a Unifying Framework for Fuzzy Logic Programming Semantics (Extended Version)
本文将经典稳定模型和良基语义重构于近似不动点理论框架内,扩展其至多值逻辑,并应用于模糊逻辑程序设计,澄清语义关系、推广分层概念并设计更精确变体。
2025-07-16 cs.LO
Combining Event Calculus and Description Logic Reasoning via Logic Programming
本文介绍了一种在逻辑程序设计框架下将事件演算与描述逻辑相结合的知识表示语言。其目的是为用户提供一种表达语言,用于建模和分析随时间演变的系统。该方法的例子与逻辑程序设计语言中实现的Fusarium系统。本文扩展了Fusarium的规则语言与描述逻辑$\cal ALCIF$的弱DL-安全接口,并使事件演算适应这种扩展语言。通过这种方式,带时间戳的ABOX可以在事件演算中作为流畅项进行操作。这一切都是在福柯的时间分层概念的框架内进行的。本文件酌情提供了健全性和完整性的条件。使用一个详细的例子,它演示了事件演算,描述逻辑和逻辑编程规则的相互作用,用于计算可能的模型作为合理的解释的建模系统的当前状态。
2021-09-10 cs.LO
Proceedings of the 8th International Workshop on Non-Monotonic Reasoning, NMR'2000
这些论文在第八届非单调推理国际研讨会(NMR2000)上发表。该系列由约翰·麦卡锡于1978年开始。第一次国际核磁共振研讨会于1984年6月在纽约州新帕尔茨的Mohonk Mountain House举行,由Ray Reiter和Bonnie Webber组织。在过去的10年里,非单调推理领域已经有了一些重要的发展。在理解非单调性的一般抽象原则方面取得了重大的理论进展。建立了非单调逻辑的可表达性和计算复杂性的关键结果。进一步阐明了非单调推理在信念修正、溯因推理、行动推理、规划推理和不确定性推理中的作用。几个成功的核磁共振系统的建立和应用,如计划,调度,逻辑编程和约束满足。会议记录中的论文反映了该领域的最新进展。它们按在讲习班上举行的特别会议分为几节:1.通用NMR轨道2。3. abduction reasonig信念修正:理论与实践4。行动与规划5。系统描述和演示6. NMR中的不确定性框架
2000-03-22 cs.AI cs.LO
Foundations of logic programming in hybrid-dynamic quantum logic
本文提出一种简单且富有表达力的混合动态逻辑用于描述量子程序,研究其中的 Horn 子句并证明初始语义定理,进而通过证明 Herbrand 定理变体奠定了该逻辑片段中量子程序逻辑编程的基础。
2024-06-04 cs.LO
In Praise of Impredicativity: A Contribution to the Formalisation of Meta-Programming
将程序作为数据处理是函数和逻辑编程的成功之一。高阶函数,如函数式编程中的程序处理程序,以及元程序,如逻辑编程中的元程序,是广泛使用的声明式编程技术。在逻辑编程中,元编程实践与其理论之间存在差距:元编程的形式化并没有明确地解决其不可预测性,并且并不充分。本文旨在克服这种不令人满意的情况,讨论的相关性impredictivity元编程,通过重新审视以前的形式化元编程和定义反射谓词逻辑,一阶逻辑的保守扩展,它提供了一个简单的形式化元编程。
2020-04-18 cs.LO
Fuzzy Linguistic Logic Programming and its Applications
本文介绍了模糊语言逻辑规划,它是由P. Vojtas提出的模糊逻辑规划与模糊对冲代数的结合,以便于对人类知识用自然语言表示和推理。在模糊语言逻辑编程中,真值是语言值,例如,VeryTrue、VeryProbablyTrue和LittleFalse,取自语言真值变量的模糊限制语代数,语言模糊限制语(修饰语)可以用作公式中的一元连接词。这是因为人类的推理主要是根据语言术语而不是数字进行的,而语言模糊限制语通常用于自然语言中以表达不同程度的强调。该文件提出:(1)模糊语言逻辑程序设计语言;(2)根据Herbrand解释和模型的声明语义;(3)直接操纵语言项计算查询真值下界并证明其可靠性的过程语义;(4)逻辑程序的不动点语义,并在此基础上证明过程语义的完备性;(v)模糊语言逻辑程序设计的几种应用;以及(vi)实现一个执行模糊语言逻辑程序的系统的想法。
2009-04-03 cs.LO
Interactive Logic Programming via Choice-Disjunctive Clauses
在逻辑编程中添加交互是一项重要任务。线性逻辑等表达逻辑为这种机制提供了理论基础。不幸的是,没有一个现有的线性逻辑语言可以建模与用户的交互。这是因为他们使用可证明性作为计算的唯一基础。我们建议使用游戏的语义,而不是可证明性作为计算的基础,让用户更积极的参与。我们说明我们的想法通过muprolog,一个扩展的Prolog与选择析取子句。
2015-07-12 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
A Meta-Programming Approach to Realizing Dependently Typed Logic Programming
依赖类型的lambda演算(如逻辑框架(LF))可以编码类型中术语之间的关系,并且可以自然地捕获公式及其证明之间的对应关系。这样的演算也可以给出一个逻辑编程的解释:LLF系统就是基于这样一个LF的解释。我们在这里考虑是否一个传统的逻辑程序设计语言可以提供一个类似的系统编码类型和证明和公式依赖的好处。特别是,我们提出了一个简单的映射从LF规范的一组公式在高阶遗传Harrop(hohh)语言,涉及推导和证明搜索之间的两个框架。然后,我们表明,这种编码可以通过利用知识的原始LF规范的良好形式,以消除大量冗余的类型检查信息。所得到的逻辑程序具有与原始规范非常相似的结构,从而允许将LF规范视为hohh元程序。使用Teyjus实现的PrologaProlog,我们表明,我们的翻译提供了一个有效的手段执行LF规范,补充的能力,PrologaProlog系统提供的推理。
2010-05-24 cs.LO
Proceedings of the 19th Workshop on Logic-based methods in Programming Environments (WLPE 2009)
本卷包含了在第19届研讨会上提出的论文基于逻辑的方法在编程环境(WLPE'09),这是在帕萨迪纳举行,美国,2009年7月14日。WLPE旨在为研究基于逻辑的方法和工具的研究人员提供一个非正式会议,以支持程序开发和分析。今年,我们继续并巩固了从逻辑编程的环境工具到一般编程的基于逻辑的环境工具的重点转移,因此这个研讨会可能对更广泛的科学界感兴趣。所有提交给WLPE'09的论文都经过了仔细的同行评审,每篇论文至少经过三次评审,随后在项目委员会进行了深入讨论。
2010-02-24 cs.LO
The Fusemate Logic Programming System (System Description)
模糊逻辑是一种逻辑编程系统,它实现了析取逻辑程序的可能模型语义。它的输入语言围绕着一个弱的分层概念,上面有理解和聚合运算符。Fusarium在Scala程序设计语言中实现为浅嵌入。这使得Scala数据类型可以作为术语使用,与外部系统的紧密接口,并且它使模型计算可以作为普通的容器数据结构构造器使用。本文描述了上述功能,并证明了他们与一个非平凡的用例,嵌入的描述逻辑$\cal ALCIF$到Fusarium的输入语言这个版本的文件纠正了一个错误的出版版本,其中使用了不合适的版本“阻塞”的$\cal ALCIF$嵌入。
2021-05-19 cs.LO
Modules and Logic Programming
我们研究的条件下,同时建设的证明网的框架开发的Andreoli在最近的论文。为此,我们定义了特定的正确性标准。我们首先研究封闭的模块(即有效性的执行一个逻辑程序),然后扩展该标准的开放模块(即有效性在执行过程中)区分标准的非循环性和可连接性,以允许增量验证。
2004-11-10 cs.LO
Proceedings 41st International Conference on Logic Programming
第41届国际逻辑编程会议记录收录了逻辑编程领域的最新研究成果,涵盖理论基础、语言设计、程序分析与应用等多个方面。
2025-12-31 cs.LO
On Answer Substitutions in Logic Programming
答案替换在逻辑编程中起着核心作用。为了支持{ \it selective}答案替换,我们将目标中的$\exists x$细化为两个不同的版本:噪声版本$\exists^o x$和无声版本$\exists x$。主要区别在于,只有$\exists^o x$中的实例化才会记录在答案替换中。$\forall x$也是如此。此外,我们还讨论了无关常数和未知常数的概念。
2018-01-27 cs.LO
Abduction with Penalization in Logic Programming
溯因最早是在经典逻辑的背景下提出的,近年来在逻辑编程领域得到了越来越多的研究。本文研究逻辑程序设计中的{带惩罚的\em溯因}。这种形式的溯因推理,以前在逻辑编程中没有分析过,结果很自然地代表了几个相关的问题,包括优化问题。我们从逻辑程序中定义了一个带惩罚的溯因推理的形式化模型,它扩展了Kakas和Mancarella提出的溯因推理框架。我们表现出这种形式主义的高表现力,通过编码一对夫妇的相关问题,包括著名的旅行商问题,从优化理论,在这个溯因框架。结果编码非常简单和优雅。我们分析了在这个框架中出现的主要决策问题的复杂性。这门课的一个有趣的结果是否定是免费的。事实上,增加(甚至是未分层的)否定并不会进一步增加溯因推理任务的复杂性(这与非自由程序相同)。
2001-11-06 cs.LO
Proceedings 29th and 30th Workshops on (Constraint) Logic Programming and 24th International Workshop on Functional and (Constraint) Logic Programming
(约束)逻辑编程研讨会(WLP)是德国逻辑编程学会(Gesellschaft für Logische Programmierung e.V.,GLP),并汇集了对逻辑编程、约束编程、答案集编程以及数据库和人工智能等相关领域感兴趣的研究人员(不仅来自德国)。函数和(约束)逻辑编程国际研讨会(WFLP)旨在汇集对函数编程,逻辑编程及其集成感兴趣的研究人员,学生和从业者。讲习班有一个共同地点的传统,以促进对高级声明性程序设计语言和相关领域的基础、应用和组合感兴趣的社区之间的跨部门思想和经验交流。
2016-12-31 cs.LO cs.PL
Dynamic Reasoning Systems
Florida State University(佛罗里达州立大学)
一个{ \it动态推理系统}(DRS)是一个传统的形式逻辑系统的适应,明确地描绘推理作为一个时间活动,与系统的每个非逻辑输入和每个推理规则的应用被视为发生在一个不同的时间步骤。每个DRS都包含一些定义良好的逻辑以及一个控制器,用于指导推理过程以响应用户输入。逻辑是通用的,而控制器是特定于应用程序的。尽管如此,每个控制器都提供了一个非单调信念修正算法。DRS的一般概念包括一个框架,在该框架内,人们可以为给定的应用制定逻辑和算法,并证明算法是正确的,即,它们用于(i)导出所有显著信息和(ii)保持信念集的一致性。本文用普通的一阶谓词演算来说明这一思想,并为此目的进行了适当的修改,以及两个例子。后一个例子重温了一些经典的非单调推理难题(企鹅作品,尼克松钻石),并显示了如何在DRS的上下文中解决这些问题,使用扩展版本的一阶逻辑,包括类型谓词符号。所有的概念都是严格定义和有效计算的,从而为未来的软件实现提供了基础。
2013-08-25 cs.AI cs.LO
(Co)recursion in Logic Programming: Lazy vs Eager
CoALP(英语:CoAlgebraic Logic Programming)是逻辑编程的一种方言,旨在为逻辑编程中的递归和共递归函数带来更精确的编译时和运行时终止和生产力分析。它的第二个目标是将类似于函数定理证明器的保护惰性(共)递归引入逻辑编程。在本文中,我们解释了CoALP的懒惰特性,并将其与CoLP中的循环分析和急切执行进行了比较。最后,我们概述了未来的发展方向,在逻辑编程的守护(共)递归。
2014-05-20 cs.LO cs.PL
Representing First-Order Causal Theories by Logic Programs
Google Inc.(谷歌公司);Arizona State University(亚利桑那州立大学);University of Kentucky(肯塔基大学);University of Texas at Austin(德克萨斯大学奥斯汀分校)
由诺曼·麦凯恩(Norman McCain)和哈德森·特纳(Hudson Turner)提出的非单调因果逻辑成为几种表达性动作语言的语义基础。McCain将确定性命题因果理论嵌入到逻辑编程中,为使用答案集求解器来回答有关此类语言描述的动作的查询铺平了道路。在本文中,我们将这种嵌入扩展到非定理论和一阶因果逻辑。
2011-03-23 cs.AI cs.LO
Syntax and semantics of multi-adjoint normal logic programming
本文提出了多伴随正规逻辑程序,通过在底层格中引入否定算子扩展了原有框架,并给出了其语法语义及确保稳定模型存在性与唯一性的充分条件。
2024-09-24 cs.LO math.LO
Proceedings 38th International Conference on Logic Programming
ICLP是展示逻辑编程研究的首要国际活动。对ICLP 2022的贡献是在逻辑编程的所有领域,包括但不限于:基础:语义学,形式主义,非单调推理,知识表示。语文问题:并发,对象,协调,移动性,高阶,类型,模式,断言,模块,元编程,基于逻辑的特定领域语言,编程技术。编程支持:程序分析、转换、验证、验证、分析、测试、执行可视化。实施情况:编译、虚拟机、存储管理、并行和分布式执行、约束处理规则、制表、外部接口、用户界面。相关范例和协同作用:归纳和共归纳逻辑编程,约束逻辑编程,答案集编程,与SAT,SMT和CSP求解器的交互,定理证明,论证,概率编程,机器学习。应用领域:数据库、大数据、数据集成和联邦、软件工程、自然语言处理、Web和语义网、代理、人工智能、计算生命科学、网络安全、机器人技术、教育。
2022-08-04 cs.AI cs.LO
A Survey of the Proof-Theoretic Foundations of Logic Programming
一些形式系统,如归结和最小模型语义,为逻辑编程提供了一个框架。在本文中,我们将调查使用结构证明理论作为替代基础。在过去的35年里,研究人员一直在使用这个基础来将逻辑编程从一阶经典逻辑的根源提升到直觉和线性逻辑的高阶版本。这些更具表现力的逻辑程序设计语言允许捕获有状态计算和丰富形式的抽象,包括高阶编程、模块化和抽象数据类型。术语级绑定是另一种抽象,在证明理论和这些扩展逻辑程序设计语言中,它们都得到了优雅而直接的处理。逻辑编程也激发了证明理论的新成果,例如涉及极性和聚焦证明的成果。这些最新的研究结果提供了一个高层次的手段,呈现前向链和后向链风格推理之间的差异。在证明论中验证逻辑编程也有助于识别它与函数式编程、演绎数据库和模型检验的联系和区别。
2021-10-30 cs.LO cs.PL
Logic Programming for Describing and Solving Planning Problems
一个逻辑编程范式,表示解决问题的稳定模型,最近已被提升为一个声明性的方法来解决各种组合和搜索问题,包括规划问题。在这种范式中,所有的程序规则被认为是约束和解决方案是稳定的模型的规则集。这与逻辑编程的标准范式有着相当大的不同。在本文中,我们重新溯因逻辑编程,并认为它允许一种编程风格,这是声明性的编程基于稳定的模型。然而,在溯因逻辑编程中,有两种规则。一方面是谓词定义(可能依赖于可溯物),它只不过是标准的逻辑程序(当包含否定时,具有非单调语义);另一方面是约束可溯物模型的规则。在这个意义上,溯因逻辑编程是逻辑编程标准范式的平滑扩展,而不是彻底的背离。
2000-03-08 cs.AI cs.LO
Introduction to the 26th International Conference on Logic Programming Special Issue
IMDEA Software Institute(IMDEA软件研究所);U. Politécnica de Madrid (UPM)(马德里理工大学);University of Potsdam(波茨坦大学)
这是第26届逻辑程序设计国际会议特刊的序言
2010-08-10 cs.AI cs.LO
Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types
余代数,霍恩子句逻辑编程和类型研讨会于2016年11月28日至29日在爱丁堡举行。该研讨会标志着EPSRC授予的类型推断的共代数逻辑编程的结束。Komendantskaya,赫瑞瓦特大学和J. Power,巴斯大学,英国。
2017-09-13 cs.LO cs.PL
Proceedings 40th International Conference on Logic Programming
University of Texas at Dallas(德克萨斯大学达拉斯分校)
该论文集收录第40届国际逻辑程序设计会议(ICLP)的技术内容,涵盖逻辑程序设计的语义、语言设计、程序分析及实现方法学等领域,展现该领域的最新研究成果。
2025-02-11 cs.AI cs.LO
Proceedings 37th International Conference on Logic Programming (Technical Communications)
ICLP是展示逻辑编程研究的首要国际活动。对ICLP 2021的贡献是在逻辑编程的所有领域,包括但不限于:基础:语义学,形式主义,非单调推理,知识表示。语文问题:并发,对象,协调,移动性,高阶,类型,模式,断言,模块,元编程,基于逻辑的特定领域语言,编程技术。编程支持:程序分析、转换、验证、验证、分析、测试、执行可视化。实施情况:编译、虚拟机、存储管理、并行和分布式执行、约束处理规则、制表、外部接口、用户界面。相关范例和协同作用:归纳和共归纳逻辑编程,约束逻辑编程,答案集编程,与SAT,SMT和CSP求解器的交互,定理证明,论证,概率编程,机器学习。应用领域:数据库、大数据、数据集成和联邦、软件工程、自然语言处理、Web和语义网、代理、人工智能、计算生命科学、网络安全、机器人技术、教育。
2021-09-15 cs.AI cs.LO
A note on the Declarative reading(s) of Logic Programming
本文分析了逻辑程序设计的说明性阅读。逻辑编程--以及作为失败的否定--没有唯一的声明性阅读。一个普遍的观点是,逻辑编程是默认推理的逻辑,默认逻辑或自动认知逻辑的子形式主义。在这种观点中,作为失败的否定是一个模态算子。在另一种观点中,逻辑程序被解释为定义。在这种观点中,作为失败的否定是经典的客观否定。从常识的角度来看,这两种观点肯定是有区别的。令人惊讶的是,这两种类型的声明性阅读都导致了相同的模型语义。本说明调查了这一情况的原因。
2000-03-13 cs.AI cs.LO
Stable models and an alternative logic programming paradigm
在本文中,我们重新审视的地方和作用的稳定模型语义在逻辑编程和对比,它与最少Herbrand模型的方法霍恩程序。我们证明了稳定模型语义的固有特征自然会导致一个逻辑编程系统,提供了一个有趣的替代更传统的逻辑编程风格的霍恩逻辑编程,分层逻辑编程和逻辑编程与良好的基础语义。所提出的方法是基于程序条款的约束的解释。在这种情况下,程序不描述一个单一的预期模型,而是一系列稳定的模型。这些稳定的模型编码解决方案的约束满足的问题所描述的程序。我们的方法对逻辑程序的语法施加了限制。特别是,函数符号被从语言中删除。我们认为,由此产生的逻辑编程系统是很好地协调NP类的问题,有一个定义明确的应用领域,和一个新兴的编程方法。我们指出,是什么使整个方法可行的算法来计算命题逻辑程序的稳定模型的实现的最新进展。
1998-09-18 cs.AI cs.LO
Tractable reasoning about Agent Programming in Dynamic Preference Logic
虽然在Agent编程领域已经提出了几种BDI逻辑,但尚不清楚这些逻辑如何连接到它们应该指定的Agent程序。更重要的是,这些逻辑中的推理问题,基于模态逻辑,一般来说是不容易处理的,限制了它们的使用来解决现实世界的问题。在这项工作中,我们使用的动态偏好逻辑BDI代理程序设计语言提供了一个语义基础,并调查这个逻辑的易处理的表达片段的原因代理程序。有了这一点,我们的目标是提供一种实现语义接地代理程序设计语言与易处理的推理周期的方式。
2019-11-14 cs.LO cs.MA
ALPprolog --- A New Logic Programming Method for Dynamic Domains
University of Oxford(牛津大学);The University of New South Wales(新南威尔士大学)
逻辑编程是一个强大的编程范例自主智能体在动态领域,如Golog和Flux语言见证。在这项工作中,我们提出了ALPprolog,一个富有表现力的,但有效的,逻辑程序设计语言的代理,必须对不完整的信息和传感器动作的原因在线控制。
2011-07-26 cs.AI cs.LO
The CIFF Proof Procedure for Abductive Logic Programming with Constraints: Theory, Implementation and Experiments
Università di Pisa(比萨大学);Imperial College London(帝国理工学院);University of Amsterdam(阿姆斯特丹大学)
给出了带约束的溯因逻辑程序设计的CIFF证明过程,并证明了其正确性。CIFF是溯因逻辑编程的IFF证明过程的扩展,放松了对变量量化(允许条件)的原始限制,并结合了约束求解器来处理约束逻辑编程中的数值约束。最后,我们描述了CIFF系统,将其与最先进的溯因系统和答案集求解器进行比较,并展示了如何使用它来编程一些应用程序。(To《逻辑程序设计理论与实践》(Theory and Practice of Logic Programming,TPLP)
2009-06-05 cs.AI cs.LO
Propositional satisfiability in answer-set programming
我们表明,命题逻辑及其扩展可以支持答案集编程的方式一样,稳定的逻辑编程和析取逻辑编程。为此,我们介绍了一个逻辑的基础上的逻辑命题图式和封闭世界假设的一个版本。我们称之为CWA(PS+,符号)命题图式的扩展逻辑。这种逻辑的一个重要特征是它支持对集合基数的约束进行显式建模。在本文中,我们刻画了一类问题,可以解决的有限PS+理论。我们实现了一个基于PS+逻辑的编程系统,并在PS+中设计和实现了一个处理理论的求解器。我们提出了令人鼓舞的性能结果,我们的方法-我们表明,它是有竞争力的模型,一个国家的最先进的答案集编程系统的基础上稳定的逻辑编程。
2001-07-19 cs.AI cs.LO