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
(Co)recursion in Logic Programming: Lazy vs Eager
CoALP(英语:CoAlgebraic Logic Programming)是逻辑编程的一种方言,旨在为逻辑编程中的递归和共递归函数带来更精确的编译时和运行时终止和生产力分析。它的第二个目标是将类似于函数定理证明器的保护惰性(共)递归引入逻辑编程。在本文中,我们解释了CoALP的懒惰特性,并将其与CoLP中的循环分析和急切执行进行了比较。最后,我们概述了未来的发展方向,在逻辑编程的守护(共)递归。
2014-05-20 cs.LO cs.PL
Mapping Objects to Persistent Predicates
Prolog逻辑程序设计在许多需要存储知识的系统中被广泛用于提供持久性。用于供应持久性的Prolog编程语言的一些实现具有与其他程序设计语言的双向接口,总体上具有面向对象的编程语言。目前,缺少用于系统开发的工具和框架,这些工具和框架以简单和敏捷的形式使用逻辑谓词持久性。更具体地说,目前需要一个面向对象和逻辑持久性提供程序,允许在主存中操作对象,并且该对象的持久性具有逻辑编程谓词方面。目前的工作介绍了一个面向对象和逻辑持久性提供者的支持对象的序言声明性映射的替代。所提出的替代方案包括逻辑编程谓词与面向对象方法的对应关系,其中对于逻辑编程的每个元素,一个面向对象的元素使其相互作用。逻辑程序设计谓词的面向对象表示提供了对组成知识的元素进行操作的便利。
2017-05-01 cs.LO cs.PL cs.SE
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
Proceedings of the 15th Workshop on Logic-based methods in Programming Environments WLPE'05 -- October 5, 2005 -- Sitges (Barcelona), Spain
本卷包含在WLPE 2005年,第15届国际研讨会在编程环境中基于逻辑的方法提出的论文。研讨会的目的是为研究基于逻辑的程序开发和分析工具的研究人员提供一个非正式会议。今年我们强调了两个方面:一方面是逻辑编程环境工具的介绍,语用学和经验;另一方面是一般编程的基于逻辑的环境工具。该研讨会在西班牙锡切斯(巴塞罗那)举行,作为第21届国际逻辑编程会议(ICLP 2005)的卫星研讨会。这次研讨会是继在美国俄亥俄州(1989年)、以色列埃拉特(1990年)、法国巴黎(1991年)、美国华盛顿(1992年)、加拿大温哥华(1993年)、意大利圣玛格丽塔利古雷(1994年)、美国波特兰(1995年)、比利时鲁汶和杰斐逊港成功举办的一系列逻辑编程环境国际研讨会之后的又一次。美国拉斯克鲁塞斯(1999年)、塞浦路斯帕福斯(2001年)、丹麦哥本哈根(2002年)、印度孟买(2003年)和法国圣马洛(2004年)。我们收到了8份提交文件(2份来自法国,2份来自西班牙-美国合作,1份来自西班牙-阿根廷合作,1份来自日本,1份来自联合王国,1份来自瑞典-法国合作)。计划委员会已决定接受七份文件。本卷包含已接受论文的修订版。我们感谢论文的作者、审稿人和项目委员会成员的帮助和富有成效的讨论。
2005-08-25 cs.LO cs.PL cs.SE
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
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
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
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
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
Fuzzy Linguistic Logic Programming and its Applications
本文介绍了模糊语言逻辑规划,它是由P. Vojtas提出的模糊逻辑规划与模糊对冲代数的结合,以便于对人类知识用自然语言表示和推理。在模糊语言逻辑编程中,真值是语言值,例如,VeryTrue、VeryProbablyTrue和LittleFalse,取自语言真值变量的模糊限制语代数,语言模糊限制语(修饰语)可以用作公式中的一元连接词。这是因为人类的推理主要是根据语言术语而不是数字进行的,而语言模糊限制语通常用于自然语言中以表达不同程度的强调。该文件提出:(1)模糊语言逻辑程序设计语言;(2)根据Herbrand解释和模型的声明语义;(3)直接操纵语言项计算查询真值下界并证明其可靠性的过程语义;(4)逻辑程序的不动点语义,并在此基础上证明过程语义的完备性;(v)模糊语言逻辑程序设计的几种应用;以及(vi)实现一个执行模糊语言逻辑程序的系统的想法。
2009-04-03 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
Interactive Logic Programming via Choice-Disjunctive Clauses
在逻辑编程中添加交互是一项重要任务。线性逻辑等表达逻辑为这种机制提供了理论基础。不幸的是,没有一个现有的线性逻辑语言可以建模与用户的交互。这是因为他们使用可证明性作为计算的唯一基础。我们建议使用游戏的语义,而不是可证明性作为计算的基础,让用户更积极的参与。我们说明我们的想法通过muprolog,一个扩展的Prolog与选择析取子句。
2015-07-12 cs.LO
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
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
Proceedings 35th International Conference on Logic Programming (Technical Communications)
自1982年在马赛举行第一次会议以来,ICLP一直是展示逻辑编程研究的首要国际活动。在逻辑编程的所有领域寻求贡献,包括但不限于:基础:语义学,形式主义,非单调推理,知识表示。语言:并发,对象,协调,移动性,高阶,类型,模式,断言,模块,元编程,基于逻辑的领域特定语言,编程技术。声明式编程:声明式程序开发,分析,类型和模式推理,部分求值,抽象解释,转换,验证,验证,编译,分析,测试,执行可视化实现:虚拟机,编译,存储管理,并行/分布式执行,约束处理规则,制表,外部接口,用户界面。相关范例和协同作用:归纳和协同归纳逻辑程序设计、约束逻辑程序设计、答案集程序设计、与SAT、SMT和CSP求解器的交互、类型推断和定理证明的逻辑程序设计技术、论证、概率逻辑程序设计、与面向对象和函数式程序设计的关系。应用领域:数据库、大数据、数据集成和联合、软件工程、自然语言处理、Web和语义网、代理、人工智能、计算生命科学、教育、网络安全和机器人技术。
2019-09-17 cs.AI cs.LO cs.PL
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
AppLP: A Dialogue on Applications of Logic Programming
Stony Brook University(石溪大学)
本文介绍了2016年逻辑编程应用研讨会(AppLP)的贡献,该研讨会于10月17日举行,与纽约市法拉盛的逻辑编程国际会议(ICLP)有关。
2017-04-07 cs.AI cs.LO cs.PL
Applications of Intuitionistic Temporal Logic to Temporal Answer Set Programming
University of Corunna, Spain(科鲁纳大学);University of Angers, France(昂热大学);University of Barcelona, Spain(巴塞罗那大学);University of Potsdam, Germany(波茨坦大学)
本文通过时态平衡逻辑探讨时态答案集编程的逻辑基础,将直觉逻辑与时态逻辑编程相结合,提出新的研究方向。
2026-03-16 cs.AI cs.LO
Proceedings 36th International Conference on Logic Programming (Technical Communications)
自1982年在马赛举行第一次会议以来,ICLP一直是展示逻辑编程研究的首要国际活动。在逻辑编程和相关领域的所有领域征求贡献,包括但不限于:-基础:语义学,形式主义,集合编程,非单调推理,知识表示。- 声明式编程:推理引擎,分析,类型和模式推理,部分求值,抽象解释,转换,验证,验证,建模,分析,测试,基于逻辑的领域特定语言,约束处理规则。- 相关范例和协同作用:归纳和协同归纳逻辑程序设计、约束逻辑程序设计、与SAT、SMT和CSP求解器的交互、用于类型推断和定理证明的逻辑编程技术、论证、概率逻辑程序设计、与面向对象和函数式编程的关系、描述逻辑、神经符号机器学习、混合深度学习和符号推理。- 实施情况:并发和分布,对象,协调,移动性,虚拟机,编译,高阶,类型系统,模块,约束处理规则,元编程,外部接口,用户界面。- 应用领域:数据库、大数据、数据集成和联合、软件工程、自然语言处理、Web和语义网、代理、人工智能、生物信息学、教育、计算生命科学、教育、网络安全和机器人技术。
2020-09-19 cs.AI cs.LO cs.PL
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
The Alma Project, or How First-Order Logic Can Help Us in Imperative Programming
Alma项目的目标是设计一种强类型约束程序设计语言,它结合了逻辑和命令式编程的优点。该项目的第一阶段是设计和实现Alma-0,这是一种小型程序设计语言,为命令式编程框架内的声明式编程提供支持。它是通过扩展Modula-2的一个子集,由逻辑编程范式启发的少量功能获得的。在本文中,我们将讨论的基本原理设计的Alma-0,由此产生的混合编程框架的好处,以及目前的工作中添加约束处理能力的语言。特别是,我们讨论的逻辑和习惯变量的作用,约束存储和程序之间的相互作用,以及需要列表。
1999-07-19 cs.LO cs.PL
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
Abstract argumentation and answer set programming: two faces of Nelson's logic
University of Nebraska Omaha(内布拉斯加大学奥马哈分校);IRIT(图卢兹计算机科学研究所);Université de Toulouse(图卢兹大学);CNRS(法国国家科学研究中心)
在这项工作中,我们表明,逻辑编程和抽象的论证框架可以解释纳尔逊的建设性逻辑N4。在这种逻辑中,我们通过形式化两个原则来做到这一点,我们称之为非矛盾推理和加强的封闭世界假设:第一个原则指出,任何信念都不能基于矛盾的证据,而后者则迫使未知和矛盾的证据都被视为错误。使用这些原则,逻辑程序设计和抽象论证框架都以模块化的方式并使用对象语言转换为构造性逻辑。逻辑程序蕴涵和抽象论证支持在翻译中遵循不矛盾推理原则成为新的蕴涵连接词。然后,攻击通过将这个新的蕴涵与强否定相结合来表示。逻辑程序设计理论与实践(TPLP)
2022-03-27 cs.AI cs.LO
A lemma on closures and its application to modularity in logic programming semantics
本文指出了单调增函数闭包的一个引理,并说明了它如何适用于定义为某个单调函数的最小不动点的语义的分解和模性。特别地,它适用于逻辑程序的许多语义。一个附录解决了夹在具有相同不动点的函数之间的(可能是非单调的)函数的不动点。
2020-08-03 cs.LO
Extended multi-adjoint logic programming
本研究提出扩展多伴随逻辑程序设计范式,纳入约束与特殊聚合算子,给出语法语义,并提出转换为多伴随正规逻辑程序的机制,建立稳定模型关联,实现相关理论的迁移应用。
2024-10-07 cs.LO math.LO
Minimum Model Semantics for Extensional Higher-order Logic Programming with Negation
University of Athens(雅典大学);University of Szeged(塞格德大学)
可拓高阶逻辑程序设计是经典逻辑程序设计的推广。这种范式的一个重要特征是它保留了传统逻辑编程的所有众所周知的属性。在本文中,我们考虑在新的范式的背景下,否定的语义。利用非单调不动点理论的一些最新结果,我们证明了每一个带否定的高阶逻辑程序都有唯一的最小无穷值模型。通过这种方式,我们获得了第一个纯粹的模型论语义的否定在可拓高阶逻辑编程。使用我们的方法,我们解决了一个老的悖论,介绍了W。W. Wadge,以证明高阶逻辑编程的语义困难。
2014-05-15 cs.AI cs.LO cs.PL
Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)
本文是一个结构介绍轻仿射逻辑,其直观的片段。轻仿射逻辑有一个多项式成本削减消除(P时间正确性),并编码所有P时间图灵机(P时间完整性)。通过引入直觉轻仿射逻辑的证明网,证明了P-时间正确性。P-Time的完整性通过一个非常紧凑的程序符号得到了充分的证明。一方面,P-Time正确性的证明描述了切割消除的复杂性是如何控制的,这要归功于利用证明网的结构属性的适当切割消除策略。这使得我们能够很好地理解“段落”模态的含义,这是轻逻辑的一个特点。另一方面,P-时间完备性的证明,以及大量的编程实例,给出了一个非平凡的任务,编程资源的限制,使用直觉轻仿射逻辑推导程序的味道。
2000-06-05 cs.LO
Logic programming: laxness and saturation
命题逻辑程序$P$可以用程序中的原子命题集合上的$P_fP_f$ -余代数来标识。相应的$C(P_fP_f)$ -余代数,其中$C(P_fP_f)$是$P_fP_f$上的余自由余代数,描述了归结导子.这种对应关系已经发展到两种方式,松散的语义和饱和的语义,局部有序的范畴和右Kan扩展的基础上,分别建模一阶程序。我们统一了这两种方法,展示它们作为互补而不是竞争,反映了逻辑编程的定理证明和证明搜索方面。在保持这种统一性的同时,我们进一步改进了松弛语义,给出了具有存在变量的逻辑程序的有限模型,并在逻辑程序中的变量和局部状态的世界之间建立了精确的语义关系。
2016-08-30 cs.LO
Probabilistic Linear Logic Programming with an Application to Bayesian Network Computations (Extended Version)
University of Southern Denmark(南丹麦大学);Roma TRE University(罗马三大学)
本文提出probLO,一种将贝叶斯网络整合到线性逻辑编程中的方法,通过多头Prolog-like方法和切片操作实现概率计算。
2026-02-24 cs.LO
An Almost Classical Logic for Logic Programming and Nonmonotonic Reasoning
介绍了一种称为N^4的一阶逻辑的模型理论。N^4并不像经典逻辑那样消除双重否定,而是减少了四重否定。N^4非常接近经典逻辑:N^4有两个真值; N^4中的蕴涵是实质性的,就像在经典逻辑中一样;否定分布在N^4中的复合公式中,就像在经典逻辑中一样。结果表明,正规逻辑程序的语义可以方便地用N^4形式化:经典逻辑Herbrand解释可以直接推广到N^4;正逻辑程序的经典最小Herbrand模型与其唯一的最小N^4 Herbrand模型一致;正规逻辑程序的稳定模型与其所谓的完全最小N^4 Herbrand模型一致.
2002-07-25 cs.LO
Bialgebraic Semantics for Logic Programming
双代数提供了一个抽象框架,包含不同类型的计算模型的语义。在本文中,我们提出了一个双代数方法的语义逻辑程序设计。我们的方法是研究逻辑程序作为反应系统,并利用抽象技术开发的设置。首先,我们使用饱和度模型的操作语义的逻辑程序作为余代数上的预层。然后,利用预层上的双代数,明确了其代数结构。由此产生的语义原来是组合方面的连接和长期替代。此外,它还编码了一个并行计算模型,其可靠性由不同线程之间的内置同步概念保证。
2015-03-27 cs.LO
Non-Termination in Term Rewriting and Logic Programming
本文在统一框架下定义循环与二元链两种非终止形式,提出检测二元链的语法判据,并通过NTI在2023年终止竞赛中与领先分析器比较验证其有效性。
2023-12-21 cs.LO
Nominal Logic Programming
名义逻辑是一阶逻辑的扩展,它为抽象语法的形式化和推理提供了一个简单的基础,模一致的重命名的绑定名称(即α-等价)。本文研究基于名义逻辑的逻辑程序设计。我们描述了一些典型的名义逻辑程序,并发展了这类程序的模型论、证明论和操作语义。除了确保实现的正确行为的兴趣,这些结果提供了一个严格的基础技术分析和推理的名义逻辑程序,我们通过例子说明。
2007-08-20 cs.LO cs.PL
Logic Programming and Logarithmic Space
我们提出了一个代数的逻辑编程,相关的证明理论,更具体地说,线性逻辑和几何的相互作用。在这个结构中,对数空间(确定性和非确定性)计算的特征是通过语法限制给出的,使用来自证明理论的单词编码。我们表明,接受一个字的观察(对应的程序中的编码)可以决定在对数空间内,通过减少这个问题的一个图的非循环。此外,我们表明,意见表达的双向多头有限自动机,一种指针机,是一个标准的模型对数空间计算。
2014-06-09 cs.LO