Transitive reasoning with imprecise probabilities
University of Rome “La Sapienza”（罗马大学（萨皮恩扎大学））；LMU Munich（慕尼黑大学）；University of Palermo（巴勒莫大学）
我们研究概率信息（弱）版本的传递性，通过使用合适的定义的默认值和否定的默认值，在设置的连贯性和不精确的概率。我们表示p-一致的序列的默认值和/或否定的默认值的g-相干的不精确概率评估的相应序列的条件事件。最后，我们证明了弱传递性的连贯概率传播规则和有效性的选择推理模式，通过证明相关的知识库的p-蕴涵。
2015-03-13 cs.AI cs.LO math.PR
A New Algorithm to Automate Inductive Learning of Default Theories
在广义概念的归纳学习中，算法应该能够将概念示例与异常和噪声数据区分开。通过递归发现异常中的模式的方法对应于学习默认理论的问题。默认逻辑是人类在常识推理中使用的逻辑。因此，人类更好地理解了习得默认理论。在本文中，我们提出了新的算法来学习非单调逻辑程序形式的默认理论。实验结果表明，该算法比传统的基于归纳逻辑程序设计的方法有了显著的改进。
2017-07-10 cs.LO
Sequent-Type Proof Systems for Three-Valued Default Logic
序列型证明系统构成了一类重要且广泛使用的演算，非常适合于分析证明搜索。在我的硕士论文中，我介绍了一种缺省逻辑的变体的序列型演算，它采用\Lukasiewicz的三值逻辑作为底层的基本逻辑。这个版本的默认逻辑是由Radzikowska提出的，解决了标准默认逻辑的一些代表性缺陷。更具体地说，在我的论文中讨论的演算公理化勇敢和怀疑的推理，这个版本的默认逻辑，分别以下的非单调推理的上下文中首次介绍的Bonatti和Olivetti，采用互补演算公理化无效的公式，照顾表达的一致性条件的默认。
2019-05-12 cs.LO math.LO
Representation Theory for Default Logic
缺省逻辑可以被看作是一种表示推理Agent的信念集族的机制。因此，它本质上是二阶的。在本文中，我们研究了一个家庭的理论作为一个默认理论的扩展集的可表示性问题。我们利用正规缺省理论给出了可表示性的完整解。我们利用任意缺省理论得到了可表示性的部分结果。我们构造了不可表示的非包含理论的可数族的例子。我们还研究了缺省理论之间的等价性概念。
1999-01-28 cs.AI 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
Borhan: A Novel System for Prioritized Default Logic
本文提出开源系统 Borhan，通过改进默认逻辑定义并记录推理三元组的解释路径，在优先默认逻辑的理论基础与实际应用之间架起桥梁。
2023-10-27 cs.LO
Redundancy in Logic III: Non-Mononotonic Reasoning
给出了限制理论和缺省理论的冗余性结果。特别是，建立一个给定的理论是否是冗余的复杂性。
2005-10-12 cs.AI cs.CC cs.LO
Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning
定量方程逻辑的框架已成功地应用于推理的载体是度量空间和操作是非扩张的代数。我们在两个正交的方向扩展这个框架：代数赋予广义度量空间结构，和操作是非扩张的提升。我们将我们的结果的代数公理化的Eukaszyk-Karmowski距离的概率分布，最近发现的应用领域的表示学习马尔可夫过程。
2022-01-22 cs.LO
Genetic Algorithms for Extension Search in Default Logic
一个缺省理论可以用它的一组似是而非的结论来表征，称为它的扩展。但是，由于缺省逻辑（Sigma_2 p-完全）的理论复杂性，如果要处理非平凡的知识库，寻找这样的扩展是非常困难的。基于自然选择原理的遗传算法已成功地应用于组合优化问题，并在搜索空间大、无易处理算法的情况下得到了应用。本文的目的是表明，从遗传算法发出的技术可以用来建立一个有效的默认推理系统。在提供了一个正式的描述的组件所需的扩展搜索的基础上遗传算法原则，我们展示了一些实验结果。
2000-02-24 cs.AI cs.LO
A logic-algebraic tool for reasoning with Knowledge-Based Systems
详细阐述了命题（布尔）逻辑指定的知识库推理的逻辑代数模型的基础。该模型是从多项式（剩余环）上的常用导数的逻辑转换中构思出来的，用于设计一种新的代数几何启发推理规则。证明了该规则的可靠性和（反驳）完备性。文中介绍了一些工具的应用。
2018-09-03 cs.LO
The lexicographic closure as a revision process
非单调推理和信念修正之间的联系是众所周知的。非单调推理领域的一个中心问题是缺省蕴涵问题，即，何时表示“如果A为真，则通常B为真”的缺省信息项被认为是从给定的这种信息项集合中得出的。对于这个问题，人们提出了许多答案，但令人惊讶的是，几乎没有人试图将其与信念修正联系起来。本文的目的是给出一个例子，说明如何可以这样的连接，显示如何词典关闭的一组默认值可能被概念化为一个过程中的迭代修订的句子集。具体来说，我们使用Nayak的修订过程。
2000-03-08 cs.AI cs.LO
Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (Technical Report)
本文利用自动机与算术公式间的细粒度对偶，将位向量自动机与代数推理结合，提出以公式导数构造自动机状态并大规模优化的量化线性整数算术求解方法，原型性能媲美甚至超过前沿 SMT 求解器。
2024-05-18 cs.LO
Splitting an operator: Algebraic modularity results for logics with fixpoint semantics
众所周知，在某些条件下，可以在稳定的模型语义下分割逻辑程序，即，将这样的程序划分为多个不同的“级别”，使得整个程序的模型可以通过为每个级别递增地构造模型来构造。类似的结果也存在于其他非单调形式主义，如自认知逻辑和缺省逻辑。在这项工作中，我们提出了一个一般的，代数分裂理论的逻辑与不动点语义。再加上近似理论的框架，一个一般的不动点理论的任意运营商，这给了我们一个统一的和强大的方式得出分裂结果的每一个逻辑与不动点语义。我们证明了这些结果的有用性，通过推广现有的结果为逻辑编程，自动认知逻辑和默认逻辑。
2006-10-26 cs.AI cs.LO
Inductive Reasoning for Coinductive Types
本文提出 AlgCo 框架，利用代数完全偏序和稠密集合上的原始递归，实现对 conats、流等余归纳类型的归纳推理，并在 Coq 中验证了筛法、正则表达式库和概率采样语义。
2023-04-07 cs.LO
Algebraic Reasoning over Relational Structures
本文针对关系结构上的代数，提出簇方程概念，证明其与抽象范畴方程等价，并给出Birkhoff型簇定理和精确性定理，分类方程表达力。
2024-12-07 cs.LO
Coming to Terms with Quantified Reasoning
有限项代数理论为描述函数语言的语义提供了一个自然的框架。有效地推理项代数的能力对于在代数数据类型（如列表和树）上对函数式或命令式程序进行自动化程序分析和验证是必不可少的。然而，由于有限项代数的理论是不可公理化的，关于项代数上的量化性质的推理是具有挑战性的。在本文中，我们解决了完整的一阶推理的程序操纵项代数的属性，并描述了两种方法，这样做，通过使用一阶定理证明。我们的第一种方法是一个保守的扩展理论的项代数使用有限数量的报表，而我们的第二种方法依赖于扩展叠加演算的一阶定理证明额外的推理规则。我们在一阶定理证明器Vampire中实现了我们的工作，并在大量代数数据类型基准测试以及博弈论约束上对其进行了评估。我们的实验结果表明，我们的方法是能够找到许多困难的问题以前未解决的最先进的方法的证明。我们还表明，吸血鬼实现我们的方法优于现有的SMT求解器能够处理代数数据类型。
2016-11-09 cs.LO
Learning of Human-like Algebraic Reasoning Using Deep Feedforward Neural Networks
Institute of Automation, Chinese Academy of Sciences（中国科学院自动化研究所）；Beijing Forestry University（北京林业大学）；Griffith University（格里菲斯大学）
在符号推理和深度学习之间有很大的差距。在这项研究中，我们探索了使用深度学习来改善符号推理的可能性。简而言之，在推理系统中，深度前馈神经网络用于在从人类产生的代数推理示例学习之后引导重写过程。为了使神经网络能够识别具有非确定性大小的代数表达式的模式，使用简化的部分树来表示表达式。此外，表示自上而下和自下而上的信息的表达式，集中化技术被用来改善减少部分树。此外，符号关联向量和规则应用记录被用来改善重写过程。实验结果表明，只有当前向神经网络具有足够的隐层时，代数推理实例才能准确地学习。此外，集中技术，符号关联向量和规则应用记录可以降低推理的出错率。特别是，上述方法导致了4.6%的出错率的推理数据集的线性方程，微分和积分。
2017-04-25 cs.AI cs.LG cs.LO
First-Order Reasoning and Efficient Semi-Algebraic Proofs
半代数证明系统，如平方和（Sum-of-Squares，SoS），由于其与近似算法的关系，近年来引起了人们的广泛关注：常次数半代数证明可以为重要的NP-难优化问题提供多项式时间近似算法的最优解。出于需要允许一个更精简和统一的框架与SoS证明比限制性命题水平的工作，我们开始了系统的一阶逻辑调查的代数和半代数证明系统的推理可能。具体来说，我们开发了一阶理论，以精确的方式捕获常次数代数和半代数证明系统：在我们的理论中可证明的某种形式的每个陈述分别转化为一族常次数多项式微积分或SoS反驳;并且使用反射原理，反之亦然。这将代数和半代数证明系统置于有界算术的既定框架中，同时提供与通常的命题逻辑系统有很大不同的系统相对应的理论。我们给出的例子，我们的半代数理论如何证明声明，如鸽子洞原则，我们提供了一个代数和半代数理论之间的分离，我们描述了最初的尝试，以超越这些理论，通过引入扩展，使用不等式符号，确定沿途的扩展导致的范围外的恒定度SoS。此外，我们证明了命题证明的新结果，特别是扩展Berkholz的动态静态模拟多项式演算（PC）的SoS PC与激进的规则。
2021-05-18 cs.CC cs.LO
Enablers and Inhibitors in Causal Justifications of Logic Programs
University of Corunna（拉科鲁尼亚大学）
出现在逻辑编程理论与实践（TPLP）中。在本文中，我们提出了一个扩展的逻辑编程（LP），其中每个默认文字来自良好的基础模型相关联的理由表示为一个代数表达式。这个表达式包含因果解释（以规则标签构建的证明图的形式）和否定范围内的术语，这些术语代表启用或禁用因果规则应用的条件。使用一些例子，我们讨论了这些新的条件，我们分别称之为“使能”和“抑制剂”，是密切相关的默认否定，并有一个本质上不同的性质，从定期的因果关系。最重要的结果是一个正式的比较，最近的代数方法的理由在LP：“为什么不种源”（WESTERN）和“因果图”（CG）。我们表明，目前的方法扩展了WESTERN和CG的理由下的基础良好的语义，作为副产品，我们还建立了这两种方法之间的正式关系。
2016-02-22 cs.AI cs.LO
Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures
Fondazione Bruno Kessler（布鲁诺·凯斯勒基金会）；Technische Universität Wien（维也纳工业大学）
处理上下文相关的知识导致了不同的形式化的概念的背景。其中之一是情境化知识库（CKR）框架，它植根于描述逻辑，但在推理方面与逻辑程序，特别是回答集编程（ASP）有很强的联系。CKR框架迎合了上下文中具有可废止公理和例外的推理，并将其扩展到覆盖（特异性）层次结构中的跨上下文知识继承。然而，该方法只支持这种单一类型的上下文关系和推理程序的工作仅限于层次结构，由于非平凡的问题与模型的偏好下的异常。在本文中，我们克服了这些限制，并提出了一个推广的CKR层次结构的多个上下文关系，以及他们的解释，可废止的公理和偏好。为了支持推理，我们使用ASP与代数措施，这是一个最近的扩展ASP加权公式半环，允许一个关联的数量与解释取决于命题原子的真值。值得注意的是，我们表明，CKR层次结构与多个上下文关系的相关片段，查询回答可以实现与流行的asprin框架。代数措施的方法是更强大的，并使例如推理与认知查询CKR，这打开了有趣的角度使用定量ASP扩展在其他应用程序。
2021-12-21 cs.AI cs.LO
Reasoning about Algebraic Data Types with Abstractions
对代数数据类型进行运算的函数的推理对于各种各样的应用来说是一个重要的问题。一个特别令人感兴趣的应用是处理或推理复杂消息结构（如XML消息）的网络应用。本文提出了一种决策过程的推理代数数据类型使用的抽象所提供的蜕变：折叠功能，映射实例的代数数据类型的值在一个可判定的域。我们表明，该过程是健全的，完全的一类退化，满足广义充分满射性条件。我们的工作扩展了以前的决策过程，展开变形函数，直到找到一个解决方案。我们使用广义充分满射性条件，以解决以前的展开算法（和相关的证明）的不完整性。然后，我们提出的单调和联想的蜕变，我们认为这提供了一个更直观的包含测试比广义充分满射条件的类别。我们使用这些概念来解决两个开放的问题，从以前的工作：（1）我们提供了一个界，相对于公式的大小，对完整性所需的展开的数量，表明它是线性的单调变质和指数小的联想变质，（2）我们证明，联想变质可以结合在一个公式，同时保持完整性。我们的组合结果扩展了可以使用基于异化的方法来推理的问题集。我们还描述了一个实现的方法，称为RADA，它接受公式的SMT-LIB 2.0语法的扩展版本。该过程是相当普遍的，是核心的推理基础设施的瓜多尔，一个特定于域的语言推理网络警卫。
2016-03-29 cs.LO cs.PL
Some Algebraic Aspects of Assume-Guarantee Reasoning
本文从代数角度研究假设-保证契约，定义契约及其运算，并揭示契约代数与布尔代数之间的函子关系以及其中的幺半群和半环结构。
2023-09-16 cs.LO cs.SY eess.SY
Structured Abductive-Deductive-Inductive Reasoning for LLMs via Algebraic Invariants
DeepThought Solutions（深思科技）；Department of Computer Science University of Florida（佛罗里达大学计算机科学系）
本文提出通过代数不变量实现LLMs的结构归纳-演绎-演绎推理框架，通过五种代数不变量确保推理链中结论的可靠性，防止逻辑不一致的累积。
2026-04-17 cs.AI cs.LG cs.LO
REBA: A Refinement-Based Architecture for Knowledge Representation and Reasoning in Robotics
University of Birmingham（伯明翰大学）；Texas Tech University（得克萨斯理工大学）；SUNY at Binghamton（纽约州立大学宾汉姆顿分校）
本文介绍了一种机器人的架构，结合了互补优势的概率图形模型和声明式编程表示和理由与逻辑为基础的概率描述的不确定性和领域知识。一个动作语言扩展到支持非布尔流畅性和非确定性的因果关系的法律。这种动作语言用于在两个粒度级别上描述紧密耦合的转换图，其中精细分辨率转换图被定义为域的粗分辨率转换图的细化。粗分辨率系统描述和包括（优先级）默认值的历史记录被转换为Answer Set Prolog（ASP）程序。对于任何给定的目标，ASP程序中的推理都提供了一个抽象的行动计划。为了实现每个这样的抽象动作，机器人自动缩放到与该动作相关的精细分辨率转换图的部分。在传感和驱动的不确定性的概率表示，然后包括在这个缩放的精细分辨率系统描述，并用于构建一个部分可观察的马尔可夫决策过程（POMDP）。通过求解POMDP获得的策略被反复调用，以将抽象动作实现为一系列具体动作，相应的观察结果被记录在粗分辨率历史中并用于后续推理。该体系结构进行评估，在模拟和移动机器人在室内域中移动对象，以表明它支持推理违反默认值，噪声观测和不可靠的行动，在复杂的领域。
2018-09-21 cs.AI cs.LO cs.RO
A note on the Declarative reading(s) of Logic Programming
本文分析了逻辑程序设计的说明性阅读。逻辑编程--以及作为失败的否定--没有唯一的声明性阅读。一个普遍的观点是，逻辑编程是默认推理的逻辑，默认逻辑或自动认知逻辑的子形式主义。在这种观点中，作为失败的否定是一个模态算子。在另一种观点中，逻辑程序被解释为定义。在这种观点中，作为失败的否定是经典的客观否定。从常识的角度来看，这两种观点肯定是有区别的。令人惊讶的是，这两种类型的声明性阅读都导致了相同的模型语义。本说明调查了这一情况的原因。
2000-03-13 cs.AI cs.LO
Local Algebraic Effect Theories
代数效应是可以用一组基本运算和它们之间的方程来描述的计算效应。由于许多有趣的效果处理程序不尊重这些方程，大多数方法假设一个微不足道的理论，牺牲了推理能力和安全性。我们提出了一种替代方法，其中类型系统跟踪在程序的子部分中观察到的方程，产生一个合理而灵活的逻辑，并为实际的优化和推理工具铺平了道路。
2020-05-27 cs.LO cs.PL
DLV - A System for Declarative Problem Solving
DLV是一个高效的逻辑编程和非单调推理（LPNMR）系统，具有先进的知识表示机制和经典关系数据库系统的接口。它的核心语言是具有完整性约束的答案集语义（Answer Set Semantics）下的析取数据库（无函数析取逻辑编程），包括默认和强（或显式）否定以及查询。还支持算术运算和各种内置谓词。此外，DLV有几个前端，即勇敢和谨慎的推理，溯因诊断，基于一致性的诊断，SQL 3的一个子集，使用动作语言进行规划，以及使用继承进行逻辑编程。
2000-03-08 cs.AI cs.LO
Algebraic Models for Qualified Aggregation in General Rough Sets, and Reasoning Bias Discovery
Indian Statistical Institute（印度统计研究所）
本文提出带近似算子格上的广义粗糙集代数聚合模型，以刻画悲观与乐观推理，并证明弱否定和蕴含结果，可用于发现推理偏差及学习歧视性行为的 ML 算法。
2023-09-22 cs.AI cs.LO math.RA
Interpolation Theorems for Nonmonotonic Reasoning Systems
克雷格插值定理（Craig's interpolation theorem，Craig 1957）是命题逻辑和一阶逻辑中的一个重要定理。它说，如果一个逻辑公式$β$在逻辑上从一个公式$α$得出，那么就有一个公式$γ$，只包括出现在两个$α,β$中的符号，这样$β$在逻辑上从$γ$得出，而$γ$在逻辑上从$α$得出。这样的定理对于理解它们所处的逻辑以及加速用这些逻辑中的理论进行推理是重要和有用的。在本文中，我们提出了插值定理在这种精神的三个非单调系统：限制，默认逻辑和逻辑程序的稳定模型语义（a.k.a.）。答案集语义）。这些结果使我们更好地理解这些逻辑，特别是与它们的非单调特性相比。他们认为，一些\emph{monotonicity}原则持有，尽管这些逻辑的经典单调性失败。此外，它们有时允许我们使用这些系统的推理分解方法，可能会增加它们的适用性和易处理性。最后，它们允许我们构建使用这些逻辑的结构化表示。
2002-07-16 cs.AI cs.LO
An Algebraic Notion of Conditional Independence, and Its Application to Knowledge Representation (full version)
Open Universiteit（开放大学）；University of Cape Town（开普敦大学）
本文在近似不动点理论的代数框架中研究了条件独立性概念，提供了独立于语言的描述，可将全局推理归约为局部推理的并行实例，并应用于正逻辑程序设计。
2024-12-18 cs.AI cs.LO
Named Models in Coalgebraic Hybrid Logic
DFKI（德国人工智能研究中心）；Universität Bremen（不来梅大学）；Imperial College London（伦敦帝国理工学院）
混合逻辑扩展了模态逻辑，支持对由所谓的名词指定的各个状态进行推理。我们在共代数语义的广泛背景下研究混合逻辑，其中Kripke框架被替换为给定函子的共代数，从而涵盖了广泛的推理原则，包括，例如，概率、分级、默认或联合运算符。具体而言，我们建立通用标准，一个给定的共代数混合逻辑承认命名的规范模型，随后的完整性证明纯扩展一方面，和扩展的混合语言与本地绑定的其他。我们用一些例子来实例化我们的框架。值得注意的是，我们证明了具有局部约束的分次混合逻辑的完备性。
2010-02-03 cs.AI cs.LO
Enriching Diagrams with Algebraic Operations
本研究通过单子的Eilenberg-Moore代数范畴富集幺半范畴，构造伴随函子，拓展带概率选择的ZX-calculus及其语义，可用于量子系统噪声的图推理。
2024-01-29 cs.LO quant-ph
Ockham's razor and reasoning about information flow
推理信息流的最小代数结构是什么？我们真的需要具有上闭包和德摩根对偶算子的布尔代数的全部能力吗？我们可以在多大程度上削弱并仍然能够以整洁的组合方式推理多智能体场景？本文提供了一些答案。
2008-08-09 cs.LO math.LO
Relations between assumption-based approaches in nonmonotonic logic and formal argumentation
Institute of Philosophy II, Ruhr Universität Bochum（波鸿鲁尔大学第二哲学研究所）；Ruhr Universität Bochum（波鸿鲁尔大学）
在本文中，我们作出的贡献，统一的形式模型的可废止推理。我们提出了几个翻译之间的正式论证框架和非单调逻辑推理合理的假设。更具体地说，我们将自适应逻辑转换为基于推理的论证，将ASPIC+、ASPIC+转换为基于推理的论证，将基于推理的论证的一个片段转换为自适应逻辑。自适应逻辑与梅金森的默认假设密切相关，并且与KLM和Shoham的偏好语义传统中的一类重要系统密切相关。因此，我们的研究结果也提供了正式的论证和后者的方法之间的密切联系。
2016-04-01 cs.AI cs.LO
A Unified Algebraic Framework for Non-Monotonicity
German University in Cairo（开罗德国大学）；Cairo University（开罗大学）
多年来，人们一直致力于深入研究非单调推理。随着非单调逻辑形式主义的丰富，一个统一的理论，使比较不同的方法是非常必要的。在本文中，我们提出了一种代数分级逻辑，称为LogAG，能够包含各种非单调形式主义。我们建立在林和Shoham的参数系统首先开发的形式化非单调常识推理。我们展示了如何编码的参数系统LogAG理论，并证明LogAG捕获的概念，相信空间的参数系统。由于参数系统捕获默认逻辑，自认知逻辑，作为失败的否定原则，和限制，我们的研究结果表明，LogAG捕获上述非单调逻辑形式主义以及。以往的结果表明，LogAG包含可能性逻辑和任何非单调推理关系满足梅金森的合理性假设。通过这种方式，LogAG为非单调性提供了一个强大的统一框架。
2019-07-22 cs.AI cs.LO cs.SC
Disjunctive Logic Programs with Inheritance
本文提出了一种新的知识表示语言DLP<，它通过继承扩展了析取逻辑程序设计（具有强否定）。继承的增加增强了语言的知识建模功能，提供了带有异常的默认推理的自然表示。给出了DLP<的一种声明性模型论语义，它推广了析取逻辑程序的回答集语义.通过对经典非单调问题的编码说明了该语言的知识建模特点。分析了DLP<的复杂性，证明了继承不会引起任何计算开销，因为DLP<中的推理与析取逻辑程序设计中的推理具有完全相同的复杂性。这一点被从DLP<到普通析取逻辑编程的有效翻译的存在所证实。使用这种翻译，一个支持DLP<语言的高级KR系统已经在DLV系统上实现，随后被集成到DLV中。
2001-06-28 cs.AI cs.LO
Quantomatic: A Proof Assistant for Diagrammatic Reasoning
Monoidal代数结构由可以具有多个输出以及多个输入的操作组成，其在许多领域中具有应用，包括范畴代数、程序设计语言语义、表示论、代数量子信息和量子群。字符串图提供了一种方便的图形语法，用于正式推理这种结构，同时避免了基于术语的方法的许多技术挑战。Quantification是一个工具，支持使用字符串图（半）自动构造等式证明。我们简要地概述了Quantity的重写引擎的理论基础，然后给出了一个概述的核心功能和架构，并给出了一个简单的例子项目，计算交换双代数的范式。
2015-10-13 cs.LO cs.MS math.CT
Complexity of Non-Monotonic Logics
Leibniz Universität Hannover（汉诺威莱布尼茨大学）
在过去的几十年中，非单调推理已经发展成为计算逻辑和人工智能领域的重要研究课题之一。已经考虑了将非单调方面引入经典逻辑的不同方式，例如，具有缺省规则的扩展、具有模态置信算子的扩展或语义的修改。在这个调查中，我们认为从上述每一种可能性的逻辑形式主义，即赖特的默认逻辑，摩尔的自我认知逻辑和麦卡锡的界限。此外，我们考虑溯因，其中一个是不感兴趣的推理，从一个给定的知识库，但在计算可能的解释观察相对于一个给定的知识库。这些逻辑的命题变体的不同推理任务的复杂性结果已经在90年代进行了研究。然而，近年来，可以观察到对复杂性问题的新的兴趣。一个当前的焦点方法是考虑参数化的问题，并确定合理的参数，允许FPT算法。在另一种方法中，重点在于识别片段，即，限制的逻辑语言，允许更有效的算法，最重要的推理任务。在本调查中，我们重点关注第二个方面。我们描述了通过限制允许的运算符集（例如，禁止否定，可以只考虑单调公式）或只考虑合取范式但具有广义子句类型的公式。我们考虑的算法问题是每个逻辑中的可满足性和蕴涵的合适变体，但也是计数问题，其中人们不仅对某些对象的存在感兴趣（例如，一个公式的模型），但要求他们的号码。
2010-09-10 cs.AI cs.CC cs.LO
Quantifying artificial intelligence through algorithmic generalization
Mathematics & Theoretical Computer Science Department, T.J. Watson Research Center, IBM Research（数学与理论计算机科学系，T.J.沃森研究中心，IBM研究）
本文提出利用代数电路复杂性理论作为量化AI算法推理能力的框架，通过计算需求定义基准，为AI科学中的算法泛化研究提供理论基础。
2025-06-19 cs.AI cs.CL cs.LG
