A temporal semantics for Nilpotent Minimum logic
在[Ban97]中指出了粗糙集(特别是准粗糙代数)与三值Rukasiewicz逻辑之间的联系。本文给出了幂零最小逻辑NM([Fod95,EG01])的一个类时态语义,其中每个时刻的逻辑都是由N_3给出的:证明了一个完备性定理。这是在[AGM08]和[ABM09]中开始的工作的继续,在这些工作中,作者为哥德尔([Göd32],[Dum59])和基本逻辑([Háj98])的多值逻辑构建了时间语义。
2013-10-22 cs.LO math.LO
Defining implication relation for classical logic
School of Software, Chongqing University(软件学院,重庆大学)
本文指出了经典逻辑中“蕴含”与“析取”等价关系存在的问题,提出了一种移除不正确“析取到蕴含”规则的逻辑系统IRL,该系统在保留经典逻辑基本定律的同时确保了该规则不可推导。
2025-05-02 cs.AI cs.CL cs.LO
Nelson algebras, residuated lattices and rough sets: A survey
本文综述了Nelson代数作为带强否定构造逻辑代数对应物在过去二十年的发展,探讨其推广N4-lattices及在对偶性和粗糙集理论中的应用,并给出基于粗糙集的表示定理。
2024-03-02 cs.LO math.LO
Defining long words succinctly in FO and MSO
我们通过一个大小为n的公式来考虑FO和MSO中可定义的最长单词的长度。对于这两个逻辑,我们得到作为这个数的上限的高度在n中线性的指数塔。我们证明了这一点计数类型相对于一个固定的量词排名。作为下限,我们得到FO和MSO的指数塔的高度在一个合理的权力n的顺序。我们显示这些下限给出具体的公式定义的累积层次结构的集合的水平的字表示。此外,我们考虑这些逻辑的Löwenheim-Skolem和Hanf数的字,并获得类似的界限,以及。
2022-02-21 cs.LO math.LO
The (Lazy) Functional Side of Logic Programming
将逻辑程序转换成功能程序的可能性一直是研究的课题。许多方法的共同点是,原始逻辑程序,为了被翻译,需要被良好地模态化,这导致了这样的共识,即这些程序可以被认为是逻辑程序的“功能部分”。因此,“复杂”逻辑变量、动态选择规则的可能性以及非良模程序的一般属性是逻辑程序的独有特征,这一点已被广泛接受。这并不完全正确,因为其中一些特性在惰性函数式语言中自然存在。我们通过定义一个适用于更广泛的逻辑程序的简单翻译,重新讨论了什么功能是逻辑编程范式所独有的老问题,并证明了目前的界限是不合理的限制。
2000-03-20 cs.LO cs.PL
The Complexity of Defining and Separating Fixpoint Formulae in Modal Logic
TU Dortmund University(多特蒙德工业大学);University of Warsaw(华沙大学)
研究模态不动点公式的模态可分离性问题,证明在不同模型类上其复杂度从PSpace-完全到TwoExpTime-完全不等,并给出分离子的有效构造算法。
2026-08-12 cs.LO
A Logic-Independent IDE
作者的MMT系统提供了一个定义和实现逻辑系统的框架。通过将MMT与jEdit文本编辑器相结合,我们获得了一个逻辑独立的IDE。IDE功能包括一些高级功能,如上下文相关的自动完成、搜索和更改管理。
2014-10-30 cs.HC cs.LO
Relational correspondences for L-fuzzy rough approximations defined on De Morgan Heyting algebras
本文研究了 De Morgan Heyting 代数上的模糊粗糙集,提出一种定理以建立模糊粗糙集与模糊关系间的对应关系,并仅用单一公理刻画了多种模糊关系复合下的模糊粗糙近似算子。
2023-10-25 cs.LO math.RA
Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic
我们提出了一个共归纳的框架,定义和推理的无穷类似物的方程逻辑和长期重写在一个统一的,共归纳的方式。该设置捕获任意序数长度的重写序列,但它既不需要序数也不需要度量收敛。这使得该框架特别适合于定理证明器中的形式化。
2018-01-09 cs.LO
Computing Abstract Distances in Logic Programs
抽象解释是执行逻辑程序的静态分析的一种成熟的技术。然而,选择提供最佳精度-成本权衡的抽象域、加宽、固定点等仍然是一个悬而未决的问题。这在很大程度上是因为在测量和比较不同分析的精度方面存在挑战。我们提出了一种新的方法来测量这样的精度,定义在抽象域的距离,并将它们扩展到一个给定的程序的整个分析之间的距离,从而允许在不同的分析精度进行比较。我们调查和扩展现有的建议,在格或抽象域的距离和度量,我们提出了一些常见的域中使用的逻辑程序分析的度量,以及扩展这些度量的空间,整个程序分析。我们在CiaoPP框架内实现这些指标,并将它们应用于衡量基准和现实程序上不同分析的精度。
2019-07-30 cs.LO cs.PL
Non-Termination of Logic Programs Using Patterns
univ-reunion(留尼汪大学)
本文提出了一种基于模式的逻辑程序非终止性检测方法,通过新展开技术生成无限集合的有限重写序列,并通过实验验证其有效性。
2026-08-10 cs.LO
Notes on applicative matching logic
本文介绍应用匹配逻辑(AML)的基本定义和结果,AML是匹配逻辑的函数变体,用于编程语言语义和程序行为推理,可作为AML理论入门文本。
2025-06-18 cs.LO math.LO
Rough concepts
本文提出了一种新的方法来统一粗糙集理论和形式概念分析。我们的方法源于模态逻辑的代数理论中发展的结果和见解,并且基于Pawlak的原始近似空间可以被视为丰富的形式背景的特殊实例的想法,即基于形式概念分析的形式背景的关系结构。
2020-02-03 cs.LO math.LO
On Deductive Systems of AC Semantics for Rough Sets
University of Calcutta(加尔各答大学)
基于反链的一般粗糙集语义是作者最近提出的。在她的论文中,两个不同的语义,一般粗糙集和另一个一般近似空间的准等价关系,开发。本文从代数逻辑的角度对这些语义进行了改进和研究。主要结果涉及的结构的代数和演绎系统的上下文中。
2016-10-09 cs.AI cs.LO math.LO
Generating proof systems for three-valued propositional logics
本文说明了如何利用 3-标号演算和 Set-Set Hilbert 风格演算,通过生成和精简子过程,为三值逻辑矩阵定义的逻辑自动生成有限公理化,并证明了两者在单演矩阵下可相互转换。
2024-01-06 cs.LO math.LO
Expressing Algorithms As Concise As Possible via Computability Logic
本文提出了一种新的算法定义和表示方法:{ \it任务逻辑}算法的概念。此概念允许用户将任务$T$的算法定义为可以共同执行$T$的一组代理。这个概念大大简化了算法开发过程,可以看作是顺序伪代码和逻辑算法的集成。这一观察结果需要对算法开发过程进行一些更改。我们提出了一个两步的方法:第一步是定义一个算法的任务$T$通过一组代理,可以共同执行$T$。第二步是将这些代理转换为(高阶)可计算性逻辑。
2013-05-09 cs.LO
Query Answering for Rough EL Ontologies (Extended Technical Report)
查询具有不完整和模糊数据的大型数据集仍然是一个挑战。基于本体的查询应答是利用本体中的背景知识对标准数据库查询应答进行扩展,以扩充不完整的数据。我们专注于本体写在粗糙的描述逻辑(DL),它允许表示模糊的知识,通过划分的话语域到类的不可辨别的元素。在本文中,我们扩展了基于本体的查询回答的组合方法的一个变种的DL EL增强粗糙的概念构造。我们表明,这种扩展保留了经典EL的良好的计算性能,并可以实现标准的数据库系统。
2018-08-06 cs.LO
Foundations of logic programming in hybrid-dynamic quantum logic
本文提出一种简单且富有表达力的混合动态逻辑用于描述量子程序,研究其中的 Horn 子句并证明初始语义定理,进而通过证明 Herbrand 定理变体奠定了该逻辑片段中量子程序逻辑编程的基础。
2024-06-04 cs.LO
Unifying Graded Linear Logic and Differential Operators
CNRS(法国国家科学研究中心)
本文提出了一种将格度线性逻辑与微分算子结合的逻辑体系,并给出了其指派模型。
2026-01-08 cs.LO
The Next 700 Relational Program Logics
我们提出了第一个框架,定义关系程序逻辑的任意一元效应。该框架是嵌入在一个关系依赖类型论,是高度表达。在语义层面上,我们提供了一个代数表示的关系规范作为一类相对单子,并通过引入关系效果的观察,映射对单子计算关系规范的方式,尊重代数结构的链接计算和规范。对于任意的关系效果观察,我们一般定义了一个健全的关系程序逻辑的核心,并解释了如何完成它的一元效果在手的一个成熟的逻辑。我们表明,这个通用的框架可以用来定义关系程序逻辑的影响,不同的状态,输入输出,非确定性,和离散概率。此外,我们表明,通过实例化我们的框架与状态和无界迭代,我们可以嵌入本顿的关系霍尔逻辑的变体,也勾画了如何重建关系Hoare类型论。最后,我们确定并克服概念上的挑战,防止以前的关系程序逻辑正确处理控制效果,是第一个提供一个关系程序逻辑异常。
2019-11-21 cs.CR cs.LO cs.PL
Stratified Counterpossible Logic
Sun Yat-sen University(中山大学)
提出SCP和SCP1两种逻辑系统,通过分层结构区分不可能性类型,处理反事实条件句中的不可能前提,并证明其可靠性与完全性。
2026-07-01 cs.LO
Communication between agents in dynamic epistemic logic
本文研究认知逻辑主体之间的交流行为。它首先通过观察所有/一些代理共享其所有信息的行为,定义转换模型的模型操作,讨论其属性,引入一种用于描述它的模态,并为后者提供公理系统。手稿的主要部分集中在一个行动,通过这个行动,一些代理人分享他们的部分信息:他们分享他们所知道的关于给定公式定义的主题的所有信息。手稿再次定义了转换模型的模型操作,讨论了它的属性,介绍了描述它的模态,并为后者提供了一个公理系统。
2022-10-10 cs.LO cs.MA
In Praise of Impredicativity: A Contribution to the Formalisation of Meta-Programming
将程序作为数据处理是函数和逻辑编程的成功之一。高阶函数,如函数式编程中的程序处理程序,以及元程序,如逻辑编程中的元程序,是广泛使用的声明式编程技术。在逻辑编程中,元编程实践与其理论之间存在差距:元编程的形式化并没有明确地解决其不可预测性,并且并不充分。本文旨在克服这种不令人满意的情况,讨论的相关性impredictivity元编程,通过重新审视以前的形式化元编程和定义反射谓词逻辑,一阶逻辑的保守扩展,它提供了一个简单的形式化元编程。
2020-04-18 cs.LO
On the existence of stable models of non-stratified logic programs
本文介绍了一个基本的结果,这是相关的答案集规划,规划。自从定义了稳定模型语义以来,第一次对存在稳定模型的逻辑程序类给出了句法刻画。这个条件对于定义新的算法来检验一致性和计算答案集,以及改进现有的系统都有实际的重要性。本文的方法是引入一个新的规范形式(任何逻辑程序都可以简化为它),把注意力集中在循环依赖上。然后,技术结果以规范形式的程序(规范程序)给出,不失一般性。结果是基于识别的周期中包含的程序,表明稳定的模型的整体程序组成的稳定模型的合适的子程序,对应于周期,并定义循环图。这个图的每个顶点对应于一个循环,每条边对应于一个句柄,它是一个文字,包含一个原子,出现在两个循环中,实际上决定了它们之间的连接。事实上,循环中句柄的真值(它作为规则的头部出现)会影响循环中原子的真值(它在主体中出现)。因此,我们可以引入句柄路径的概念,连接不同的循环。如果对每个奇循环都能找到具有一定性质的句柄路径,则保证了稳定模型的存在性。
2004-12-23 cs.AI cs.LO
A Short Remark on Analogical Reasoning
Aix-Marseille Université(艾克斯-马赛大学);CNRS(法国国家科学研究中心)
我们讨论了类比推理的逻辑定义问题,并以反事实条件句、优先结构等的语义学形式给出了一个解决方案。
2019-10-06 cs.AI cs.LO
Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory [Extended Version]
TU Dresden(德累斯顿工业大学);Open Universiteit(荷兰开放大学);University of Cape Town(开普敦大学);ScaDS.AI Center for Scalable Data Analytics and Artificial Intelligence, Dresden/Leipzig(萨克森可扩展数据分析和人工智能中心)
本文利用近似不动点理论框架,为同时包含失败否定和强否定的模糊逻辑程序定义良好行为的语义,并证明该框架推广了多种现有语义并产生新语义。
2026-07-31 cs.LO
A General Automata Model for First-Order Temporal Logics (Extended Version)
University of Udine(乌迪内大学);Free University of Bozen-Bolzano(博尔扎诺自由大学)
本文定义并研究了一阶自动机模型,证明其能捕获任意FOLTL公式且具有运算封闭性与半可判定性,并以更简明的证明确立了monodic FOLTL的可判定性。
2026-11-11 cs.LO
Normal-order reduction grammars
我们提出了一个算法,对于给定的$n$,生成一个明确的规则树语法定义的组合逻辑术语的集合,在一组$\{S,K\}$的原始组合子,需要正是$n$正常的顺序减少步骤规范化。作为Curry和Feys的标准化定理的结果,我们的归约文法形成了一个完整的语法表征规范组合逻辑术语。利用它们,我们提供了一种构造普通生成函数的递归方法,该方法计算在$n$正规阶约简步骤中约简的$S K$ -组合子的数目。最后,我们调查的大小生成的文法,给出一个原始的递归上界。
2016-06-02 cs.LO
A New Modal Framework for Epistemic Logic
Peking University(北京大学)
近年来,非标准认知逻辑(knowingwhether,knowinghow,knowingwhat,knowingwhy等)引起了人们越来越大的兴趣,这些逻辑中引入的新的认知模态在语义上都共享$\exists x \Box ϕ$的一般模式,例如,知道如何实现$ϕ$大致意味着存在一种方法,这样你就知道它是一种方法,以确保$ϕ$。此外,由此产生的逻辑是可判定的。受这些特定逻辑的启发,在这项工作中,我们提出了一个非常通用和强大的框架的基础上,量词自由谓词语言扩展了一个新的模态$\Box^x$,它包完全$\exists x \Box$在一起。我们表明,所得到的语言,虽然更有表现力,共享许多良好的性质的基本命题模态逻辑在任意模型,如有限树模型属性和van Bentham的特征w.r.t.一阶模态逻辑我们公理化的逻辑在S5框架与直观的公理捕捉之间的相互作用$\Box^x$和知道,运营商在认知设置。
2017-07-27 cs.AI cs.LO
A monotone connection between model class size and description length
本文将模型类的大小与其定义公式的最小长度联系起来,即与其描述的复杂性联系起来。限制到一个固定的域的大小为n的模型,我们研究描述的复杂性与命题逻辑的扩展与计数分配的能力。这种逻辑称为GMLU,也可以被认为是Kripke模型上的分级模态逻辑。虽然GMLU是表达完整的定义多集的分配,我们也研究它的片段GMLU(d),只能计数到整数阈值d。我们特别关注GMLU(d)的等价类的描述复杂性。我们表明,在限制的偏序集的类型实现,基于大小的等价类的顺序是相同的顺序基于描述复杂性。这也证明了模型类的玻尔兹曼熵和描述复杂性之间的单调联系。此外,我们刻画了域大小n和计数阈值d之间的关系如何决定是否存在一个支配类,这实质上意味着一个模型类的极限概率为1。为了得到我们的结果,我们证明了新的估计r-相关的斯特林数。作为另一个重要的工具,我们表明,模型类分为两个不同的情况下,其描述的复杂性。
2023-01-31 cs.LO math.LO
Generalized Ideals and Co-Granular Rough Sets
University of Calcutta(加尔各答大学)
在过去的几年里,很少有人使用格论理想来定义和生成一般近似空间上的非粒度粗糙近似。这些研究的目标,在基于关系的粗糙集,已获得良好的性能相比,经典的粗糙近似。在本文中,作者对这些思想进行了严格的概括,并对相关的语义特征进行了研究,将粒用于隐式近似的构造,从而引入了共粒度的概念。知识解释相关的方法也进行了研究。这项研究将是相关的一些逻辑代数方法粗糙集,从逐点定义的近似值,并使用替代近似在空间mereological背景下,涉及实际的接触关系。本作者在早期论文中发明的基于反链的语义也适用于所考虑的上下文。
2017-04-18 cs.AI cs.IT cs.LO
Dialectical Rough Sets, Parthood and Figures of Opposition-1
University of Calcutta(加尔各答大学)
从一个角度来看,本研究的主题围绕着一般粗糙集的背景下,有关的粗糙基的存在性在一个上下文中的近似的逆问题。粒算子空间及其变体是作者最近提出的一种基于反链的一般粗糙集代数语义及其反问题的优化框架。在这个框架中,清晰和非清晰对象的各种子类型是可识别的,这些子类型在更严格的形式主义中可能会被遗漏。这也是因为在后一种情况下,补充和否定的概念被认为是理所当然的,而在现实中,它们有一个复杂的辩证基础。这激发了一个一般的方法,辩证粗糙集建设本作者以前的工作和数字的反对。本文从语义学的角度创立了辩证粗糙逻辑,形式化了辩证谓词的概念,建立了辩证谓词与辩证思维和贪婪否定的联系,并从古典和辩证对立的角度分析和研究了父子关系。她的方法变得更加几何化,并将亲子关系作为代数语义的主要关系(而不是大致等价的对象)。
2018-11-22 cs.AI cs.IT cs.LO
Comparing Dependencies in Probability Theory and General Rough Sets: Part-A
University of Calcutta(加尔各答大学)
本文作者在最近的一些论文中提出了将一般粗糙集与概率论中的依赖概念进行比较的问题。这一问题涉及到确定在确定概念方面的方法和可能性之间转换的局限性。本文作者从基于集合赋值的最简主义观点出发,对这两种方法中的依赖思想进行了比较。偏差概率框架就是这种方法的结果。其他贝叶斯推理观点(涉及数值估值)和频率论方法也是已知的。在这项研究中,对偶性的结果是适应证明的可能性,改进的比较跨之间的影响本体论不同的概念,在一个共同的逻辑为基础的框架,由本作者。积极和消极的结果都证明了她以更清晰的方式界定了可能的比较。
2018-04-06 cs.AI cs.IT cs.LO