A temporal logic of epistemic and normative justifications, with an application to the Protagoras paradox
本研究结合带过去与未来模态的线性时态逻辑与道义辩护逻辑，构建含两类辩护断言的推理框架，给出两种语义并证明公理系统的可靠性与完备性，还形式化分析了普罗泰戈拉悖论。
2021-09-21 cs.LO
The Complexity of Non-Iterated Probabilistic Justification Logic
逻辑PJ是一个概率逻辑，通过添加（非迭代）的概率运算符的基本理由逻辑J。在本文中，我们建立了上界和下界的逻辑PJ的可导性问题的复杂性。本文的主要结果是PJ中的可导性问题的复杂性与底层逻辑J中的可导性问题的复杂性保持相同，这是PJ中的可导性问题的复杂性，是PJ中的可导性问题的复杂性是PJ中的可导性是PJ中这意味着，概率运算符不会增加逻辑的复杂性，尽管它们可以说丰富了语言的表达能力。
2018-07-05 cs.LO
Some Notes on Temporal Justification Logic
证明逻辑是模态类逻辑，具有记录句法结构中模态的原因或证明的额外能力，称为证明项。证明逻辑可以被看作是模态逻辑的显式对应物。分布式系统中Agent的行为和交互通常使用知识和时间逻辑来建模。在本文中，我们勾勒出一些初步的想法，如何模态知识的知识和时间的逻辑的一部分，可以用一个适当的理由逻辑。
2015-10-25 cs.LO math.LO
A Logic of Knowledge and Justifications, with an Application to Computational Trust
Center for Logic, Language and Cognition, Department of Philosophy and Education Sciences, University of Turin（都灵大学哲学与教育科学学院逻辑、语言与认知中心）
本研究提出一种基于量化认知与证立逻辑的框架，通过非标准同一性处理刻画计算信任的超内涵性，给出证明系统与框架语义并证明可靠性完备性，为计算信任的形式化理论提供逻辑基础。
2026-11-10 cs.LO
Justification logic enjoys the strong finite model property
我们观察到，证明逻辑享有一种形式的强有限模型性质（有时也称为小模型性质）。因此，我们得到的判定性证明理由逻辑，不依赖于波斯特定理。
2015-06-23 cs.LO math.LO
Necessity as justified truth
我们提出了一个逻辑推理的必要性和理由，这是独立于关系语义。我们选择理由的概念-来自一类“理由逻辑”（Artemov 2008，Fitting 2009）-作为必要性概念所基于的原始概念。我们的公理化扩展了Suszko的非Fregean逻辑SCI（布朗，Suszko 1972）的基本公理从证明逻辑，公理量化的命题和理由，以及一些进一步的原则。核心公理是：$φ$必然为真当且仅当存在$φ$的证明。也就是说，必要性是可以通过证明来一阶定义的。而不是定义纯粹的代数模型（布朗，Suszko 1972）的风格，我们扩展了语义研究（Lewitzka 2012）的一些代数结构处理的理由，并证明我们的演绎系统的可靠性和完整性。此外，如果我们将公理模式$\squareφ\to \square\squareφ$和公理必然性规则加入到我们的系统中，我们就能够恢复模态逻辑的必然性原则。作为主要结果，我们表明，模态逻辑S4和S5可以捕获我们的语义，如果我们施加相应的模态逻辑原则作为额外的语义约束。这将遵循从证明理论的考虑和我们的完备性定理。对于系统S4，我们也给出了一个纯模型论的证明。
2012-06-03 cs.LO
Modular Models for Intuitionistic Justification Logic
我们提出的逻辑iJT 4，这是一个显式版本的直觉S4和建立健全性和完整性方面的模块化模型。
2016-04-25 cs.LO math.LO
A Note on Fixed Points in Justification Logics and the Surprise Test Paradox
本文研究了在调整逻辑中加入不动点的效果。我们介绍了两种扩展的理由逻辑：扩展的不动点（或对角）运营商，和扩展的最少不动点。前者是Smorynski的对角化算子逻辑的证明版本，后者是Kozen的模态$μ$ -演算的证明版本。我们还介绍了Fitting的量化证明逻辑的不动点扩展，并在这些扩展中形式化了Knower Partial和Surprise Test Partial。通过将惊奇陈述解释为没有正当性的陈述，我们给出了数量化证明逻辑中惊奇测试paragraph的自指版本的一个解决方案。我们也给出了形式化的惊喜测试Parket在时间模态认知逻辑，并在哥德尔-勒布证明逻辑。
2015-02-01 cs.LO math.LO
Justification Logic for Intuitionistic Modal Logic (Extended Technical Report)
本文为Fischer Servi的直觉主义模态逻辑IK及其扩展提供证明逻辑对应物，通过扩展证明项语法、公理化和无切嵌套序列系统实现语法实现。
2025-07-12 cs.LO math.LO
NEXP-completeness and Universal Hardness Results for Justification Logic
我们提供了一个较低的复杂性约束的多智能体的理由逻辑的可满足性问题，建立从我们以前的工作一般NEXP上限是紧的。然后，我们使用一个简单的修改相应的减少证明，满足所有多代理的理由逻辑从那里是很难的西格玛2 p类的第二层次的多项式-给定某些合理的条件。我们的方法改进了这些所需的条件，为同一个下界的单代理的理由逻辑，证明了巴斯和库兹涅茨在2009年，从而回答了他们的一个开放的问题。
2015-03-01 cs.CC cs.LO
Towards a Formalisation of Justification and Justifiability
我们介绍的逻辑QKSD，这是一个正常的多模态逻辑超过1000模态，另外支持有界量化的模态。这种逻辑的一个重要特征是，它允许对系统的信息组件进行量化，因此可以用于推导理由。我们比较建议的逻辑与Artemov的理由逻辑，也报告了一个原型实现的可满足性求解器的这种逻辑，并显示了一些例子。
2021-10-25 cs.LO cs.MA
Labeled Sequent Calculus and Countermodel Construction for Justification Logics
本文针对证明逻辑及混合模态-证明逻辑提出加标序列演算，内化Fitting模型语义，证明其弱子公式性质、规则可逆性等性质，建立可靠性完备性，给出可终止的证明搜索与反模型构造流程及模型对应关系。
2014-11-05 cs.LO math.LO
Tableau Proof Systems for Justification Logics
本研究针对多种证明逻辑构建Tableau证明系统，证明其相对于Mkrtychev模型的可靠性与完备性，通过句法证明实现切消以支撑完备性，还验证了系统的子公式性质，为证明逻辑的推理研究提供了形式化工具。
2016-04-11 cs.LO math.LO
On semantics of first-order justification logic with binding modalities
Steklov Mathematical Institute of Russian Academy of Sciences（俄罗斯科学院斯捷克洛夫数学研究所）
本文提出一种结合证明术语和绑定模态的第一次序逻辑证明系统，并建立了其相对于Kripke式语义的正确性和完备性。
2025-12-08 cs.LO math.LO
Justification Logic of the Lambda Calculus
Faculty of Technical Sciences, University of Novi Sad（诺维萨德大学技术科学学院）；Mathematical Institute of the Serbian Academy of Sciences and Arts（塞尔维亚科学院数学研究所）；School of Computer Science, University of Birmingham（伯明翰大学计算机学院）
研究λ演算的证明逻辑，通过引入一种逻辑，其模态证明项为类型化λ项，能同时推理计算与证明。给出公理系统、自然演绎系统及Curry-Howard解释，还构建相继式演算并证明切割消去，得到归一化结果。
2026-07-28 cs.LO math.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
Causal Graph Justifications of Logic Programs
University of Corunna（拉科鲁尼亚大学）；Vienna University of Technology（维也纳工业大学）
在这项工作中，我们提出了一个多值扩展的逻辑程序下的稳定模型的语义，在一个模型中的每个真正的原子与一组理由。这些理由表示的因果关系图形成的规则标签和边缘，代表他们的应用程序排序。对于正的程序，我们表明，一个给定的原子获得的因果理由有一个直接的correspondence- dence（相关）的语法证明，该原子使用的程序规则中涉及的图形。最有趣的贡献是，这种因果信息是在一个纯粹的语义的方式，通过代数运算（产品，总和和应用程序）的因果值格的顺序关系表示时，一个理由是强于另一个。最后，对于有否定的程序，我们通过引入一个类似于Gelfond和Lifschitz的程序约简的变换，定义了因果稳定模型的概念。因此，缺省否定表现为“证据缺失”，否定升得不到任何证明
2014-09-25 cs.AI cs.LO
Efficient Approximation of Well-Founded Justification and Well-Founded Domination (Corrected and Extended Version)
许多原生ASP求解器利用无基集通过某种形式的有据否定来计算逻辑程序的结果，但由于计算成本而忽略其逆置、有据证明（WFJ）。然而，我们证明，这可能会阻碍传播的许多相关条件，如可达性。为了执行WFJ与低计算成本，我们设计了一种方法，近似其后果计算支配者在流图中，线性时间算法存在的问题。此外，我们的方法允许额外的无根据集合推理，称为良基支配（WFD）。我们表明，WFJ和WFD的效果可以模拟的一类重要的逻辑程序，包括可达性。本文是第12届逻辑编程和非单调推理国际会议（LPNMR 2013）上发表的一篇论文的修正和扩展版本。它已被修改以排除定理10及其后果，但提供了所有缺失的证明。
2013-09-10 cs.LO
Justifications for Programs with Disjunctive and Causal-choice Rules
在本文中，我们研究了一个扩展的稳定的模型语义的析取逻辑程序在一个模型中的每个真正的原子与一个代数表达式（规则标签），代表其理由。在我们以前的工作中的非析取程序，这些理由是在一个纯粹的语义的方式，通过代数运算（产品，除了和应用程序）的因果值格。我们的新定义扩展了因果稳定模型的概念，析取逻辑程序，并满足每个（标准）稳定模型对应于一类不相交的因果稳定模型共享相同的真值分配，但可能会改变所获得的解释。我们提供了一对说明性的例子，显示新的语义的行为，并讨论了需要引入一种新的类型的规则，我们称之为cabinet的选择。这种类型的规则直观地捕捉了“$A$可能导致$B$“的想法，并且当忽略因果信息时，相当于标准稳定模型语义下的通常选择规则。（正在考虑出版在逻辑编程的理论与实践）
2016-10-11 cs.LO
Explicit Evidence Systems with Common Knowledge
本文开发了一种包含个体与公共知识证据项的多智能体证明逻辑，定义了 Kripke 风格语义并证明其可靠性与完备性，同时分析了其与 S4 的关系及协调攻击问题。
2010-05-04 cs.LO math.LO
Non-classical Topological Evidence Logic
Institute of Computer Science, Czech Academy of Sciences（捷克科学院计算机科学研究所）
本文研究将拓扑证据逻辑（TEL）扩展到非经典命题逻辑基础（直觉主义和相干逻辑），通过添加全局模态或补集内部算子，证明相干性证成可在这些非经典框架中表达，并给出相干TEL基于弱相干模态逻辑BS4的完备性定理。
2026-07-01 cs.LO
Dynamic Conflict Resolution Using Justification Based Reasoning
我们研究的冲突情况下，动态出现在交通情况下，不同的代理人试图实现自己的一套目标，并决定做什么的基础上，他们当地的看法。我们区分了此设置的几种冲突类型。为了使冲突的情况和冲突的原因建模，我们提出了一个逻辑框架，采用认知和模态逻辑，理由和时序逻辑的概念。使用这个框架，我们说明了如何识别冲突，以及我们如何得到一个链的理由，导致这种冲突。我们讨论了如何解决冲突时，车辆有本地的，不完整的信息，车辆到车辆的通信（V2V）和部分有序的目标。
2019-10-31 cs.LO cs.MA
Extensions to Justification Theory
KU Leuven（鲁汶大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
证明理论是非单调逻辑语义学的统一框架。它建立在证明的概念上，直观地说，证明是一个解释结构中某些事实的真值的图。证明理论所涵盖的知识表示语言包括逻辑程序、论证框架、归纳定义、嵌套归纳和共归纳定义。此外，理由也用于实施目的。它们用于计算现代ASP求解器中的无基集，可用于检查完整搜索算法中原子的相关性，最近的惰性接地算法构建在它们之上。在这个扩展的抽象，我们奠定了可能的扩展证明理论。
2019-05-09 cs.AI cs.LO
Exploiting Game Theory for Analysing Justifications
KU Leuven（鲁汶大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
理据理论是一个统一的语义框架。虽然它起源于非单调逻辑，但它可以应用于计算机科学的各个领域，特别是可解释推理;它最核心的概念是证明：解释为什么一个属性在模型中成立（或不成立）。在本文中，我们继续研究的理由理论的三个主要贡献。第一部分研究了辩护理论与博弈论的关系。我们证明，理由框架可以被看作是一种特殊类型的游戏。建立的联系为我们接下来的两个贡献提供了理论基础。第二个贡献是研究在什么条件下两种不同的证明理论方言（图作为解释与树作为解释）重合。第三个贡献是建立了一个精确的标准时，语义诱导的理由理论产生一致的结果。在过去，要证明这样的语义是一致的，需要繁琐而复杂的证明。我们表明，这些标准确实满足所有常见的语义逻辑编程。本文正在考虑接受逻辑编程理论与实践（TPLP）。
2020-08-04 cs.AI cs.LO
Explicit non-normal modal logic
针对道义模态的超内涵性问题，本文提出作为非正规模态逻辑超内涵对应物的新型证成逻辑，证明其可靠性与完全性，并研究实现问题。
2023-08-11 cs.LO
An Improved Proof-Theoretic Compilation of Logic Programs
在以前的工作中，我们表明，逻辑编程编译可以给出一个通用的抽象逻辑程序设计语言的证明理论的理由，并证明了这种技术的情况下，遗传Harrop公式及其线性变体。编译后的子句本身就是逻辑公式，除了在与它们的头相匹配的原子目标上存在二阶抽象。在本文中，我们重新审视我们以前的结果，以更详细和更充分的逻辑理由，消除这种虚假的抽象。然后，我们改进所得到的技术，以有效地支持模式良好的程序。
2012-10-05 cs.LO cs.PL
A logic of interactive proofs
本文提出概率双主体证成逻辑 IPJ，以支持对执行交互式证明的主体进行推理，并通过可忽略函数参数化分析概率增长，进而给出零知识证明的新概念。
2023-09-26 cs.LO
A classical-logic view on a paraconsistent logic
本文研究次协调一阶逻辑 LPQ$^{\supset,\mathsf{F}}$，提出其自然演绎证明系统，通过嵌入一阶经典逻辑提供模型论与逻辑论证，并探讨其可判定性及逻辑性质，揭示其与经典逻辑的紧密联系。
2025-09-16 cs.LO math.LO
Semantics for a Logic of Presuppositions
1952年，P.F.斯特劳森提出了一种预设逻辑。它是对阿伦特逻辑的一种解释，即对传统三段论逻辑的一种解释。1981年，理查德·迪亚兹（Richard Diaz）出版了一本专著，其中他提出了真理相关逻辑。本文指出真值相关逻辑只是预设逻辑的一个命题版本。使用真值相关逻辑，发展了一种预设逻辑的语义学。语义，然后进一步扩展到多元逻辑和一些后果进行了讨论。
2023-02-16 cs.LO
Combining Fixed-Point Definitions and Game Semantics in Logic Programming
具有定点定义的逻辑程序设计是传统逻辑程序设计的一个有用的扩展。固定点定义可以捕获简单的模型检验问题和封闭世界假设。它的操作语义通常基于直觉可证明性。我们扩展了这些语言的操作语义与游戏语义。这种扩展的语义有几个有趣的方面：特别是，它为$read$谓词提供了逻辑状态。
2015-08-05 cs.LO
A Game Theoretical Semantics for Logics of Nonsense
无意义逻辑允许第三个真值来表达\emph{nonsense}的命题。这些逻辑是理解程序中如何处理错误以及错误一旦出现如何在整个程序中传播的理想形式。本文给出了无义逻辑的Hintikkan博弈语义，并证明了它的正确性。我们还讨论了如何在博弈论中的一个已知的解决方案的方法，严格劣势策略的迭代消除，涉及到语义游戏的逻辑废话。最后，我们仅用语义游戏的方法扩展了无意义逻辑，发展了一种新的无意义逻辑，并为Priest的Parabel逻辑提出了一种新的游戏语义。
2020-09-23 cs.LO
Incorporating Inductions and Game Semantics into Logic Programming
归纳和博弈语义是对传统逻辑程序设计的两个有用的扩展。具体地说，归纳法可以捕获逻辑编程中更广泛的一类可证明公式。采用博弈语义可以使逻辑编程更具交互性。在本文中，我们提出了一个执行模型的逻辑语言与这些功能。这种执行模型密切遵循现实生活中的推理过程。
2015-08-08 cs.LO
A Model-Theoretic Semantics for Defeasible Logic
可废止逻辑是一种有效的可废止推理逻辑。它是通过证明理论定义的，到目前为止，还没有模型理论。本文给出了可废止逻辑的模型论语义。在语义方面，逻辑是健全的和完整的。我们还简要概述了这种方法如何扩展到广泛的可废止逻辑。
2002-07-25 cs.LO
Coalgebraic trace semantics via forgetful logics
我们使用模态逻辑作为一个框架，共代数迹语义，并显示了具体的例子，如加权，交替和树自动机的语言语义的方法的灵活性，和生成概率系统的迹语义。我们提供了一个充分条件下，通过一个给定的确定性建设获得的逻辑语义符合跟踪语义。最后，我们考虑一个条件，保证存在一个规范的确定过程，是正确的，相对于一个给定的逻辑语义。这个过程与Brzozowski的最小化算法密切相关。
2016-12-27 cs.LO
Games for Hybrid Logic -- From Semantic Games to Analytic Calculi
博弈语义学和获胜策略为语义学和逻辑证明系统之间提供了一个潜在的概念桥梁。我们说明了这种联系的混合逻辑-模态逻辑的扩展，允许显式引用的语言中的世界。主要的结果是，系统的搜索所有模型的获胜策略可以被有限化，从而重新制定为一个证明系统。
2022-06-01 cs.LO
An Intuitionistic Linear Logical Semantics of SAND Attack Trees
本文介绍了直觉线性逻辑中SAND攻击树的一种新的逻辑基础。这个新的基础是基于一个新的逻辑称为攻击树线性逻辑（ATLL）。在介绍ATLL之前，我们给出了几种新的攻击树逻辑模型，第一种是基于真值表的攻击树逻辑模型。然后，我们把这种语义提升为一种基于线性的攻击树语义，它引入了蕴涵，但这可以进一步提升为ATLL所基于的辩证模型。ATLL的一个重要特征是它支持顺序合取的完全分布性。
2018-01-21 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
Approximation Fixpoint Theory as a Unifying Framework for Fuzzy Logic Programming Semantics (Extended Version)
本文将经典稳定模型和良基语义重构于近似不动点理论框架内，扩展其至多值逻辑，并应用于模糊逻辑程序设计，澄清语义关系、推广分层概念并设计更精确变体。
2025-07-16 cs.LO
Semantics and Axiomatization for Stochastic Differential Dynamic Logic
在André Platzer的工作基础上，我们提出了一种随机微分动态逻辑的形式语言，并定义了它的语义、公理和推理规则。与以前的努力相比，我们的帐户的随机微分动态逻辑遵循更接近，更兼容的常规微分动态逻辑的传统帐户。我们解决了一个问题，明确的原始工作的语义，同时展示了如何使逻辑更有表现力，将不确定性的选择，明确的描述和差分条款。明确的描述需要使用三值真值语义。我们还给出了随机微分动态逻辑的第一个一致替换演算，使得它在证明助手中的实现更加实用。
2021-04-29 cs.LO
Category-theoretical Semantics of the Description Logic ALC (extended version)
范畴论可以用来陈述一阶逻辑中的公式，而不需要使用集合成员。逻辑学中的几个显著结果，如连续统假设的证明，可以在范畴论中优雅地重写。本文提出用范畴语言重新表述描述逻辑$\mathcal{ALC}$通常的集合论语义。在这种设置中，ALC概念被表示为对象，概念包含被表示为箭头，并且成员关系被表示为类别的对象和箭头上的逻辑量词。这种范畴理论语义提供了$\mathcal{ALC}$的语义的更模块化的表示和设计用于推理的算法的新方法。
2022-04-18 cs.LO
Two Remarks about Game Semantics of Classical Logic
University of Gothenburg（哥德堡大学）
本文介绍了Stefano Berardi关于经典逻辑游戏语义的两个未发表注记，并对其进行了解释。
2026-03-04 cs.LO
On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics
本文为存在二阶逻辑及团队语义逻辑的并闭片段提供语法刻画，引入包含-排除博弈作为模型检验博弈，并定义团队原子以精确捕获并闭片段，解答了开放问题。
2021-07-29 cs.LO
Polyteam Semantics
团队语义是现代依赖和独立逻辑的数学框架，其中公式由赋值集（团队）解释，而不是一阶逻辑中的单个赋值。为了加深团队语义和数据库依赖理论之间富有成效的相互作用，我们定义了“多队语义”，其中公式在一个家庭的团队进行评估。我们首先定义了一个新的polyteam变体的依赖原子，并给出了相关的蕴涵问题的有限axiomatisation。我们涉及多队语义的团队语义和调查的情况下，前者的逻辑可以模拟逻辑在后者。我们还通过存在二阶逻辑（ESO）中向下封闭和可定义的多队的性质来证明多依赖逻辑的表达能力。类似的结果是持有多独立逻辑和所有ESO定义的属性。我们还将多包含逻辑与最大不动点逻辑联系起来。
2020-03-26 cs.LO
Transfer of semantics from argumentation frameworks to logic programming A preliminary report
有各种有趣的语义（扩展）的论证框架设计。它们能够赋予一个含义，例如，到奇数周期。我们的主要动机是通过缺省否定将Baroni，Giacomin和Guida提出的奇长循环结构的语义转换为奇长循环的逻辑程序。发达的建设更加强大。对于一个给定的逻辑程序的论证框架的定义。该构造使得能够将所得到的论证框架的每个语义转换为给定逻辑程序的语义。建设的弱点进行了讨论，并概述了这种方法的一些未来的延续。
2011-08-26 cs.LO
Tractability frontiers in probabilistic team semantics and existential second-order logic over the reals
概率团队语义是概率依赖的逻辑分析框架。我们的重点是概率包含逻辑及其扩展的公理化，复杂性和表达性。我们确定了一个自然片段的存在性二阶逻辑与添加剂真正的算术，准确地捕捉概率包含逻辑的表达能力。此外，我们将这些形式主义的线性规划，这样做得到PTIME数据复杂度的逻辑。此外，在有限结构上，我们证明了具有加性实算术的完全存在二阶逻辑只能表示NP性质。最后，我们在原子层次上给出了概率包含逻辑的一个合理而完整的公理化。
2021-12-21 cs.LO
Coalgebraic Semantics for Probabilistic Logic Programming
本文提出概率逻辑编程的余代数语义，通过函子F的余代数建模程序，并利用余自由余代数给出推导树与可能世界两种语义，可恢复分布语义，并扩展至加权逻辑编程。
2021-04-09 cs.LO
Disjunction and modular goal-directed proof search
本文研究了一阶多模态逻辑中的目标导向证明搜索。关键的问题是设计一个证明系统，尊重模块性和局部性的假设，许多模态逻辑。通过强制歧义被独立地考虑，特别是模块化的析取可以被用来构建有效的可执行规范的推理任务，涉及部分信息，否则可能需要禁止搜索。为了实现这一行为，需要事先证明理论的理由逻辑编程扩展，加强，并结合证明理论分析模态演绎以一种新的方式。
2002-06-05 cs.LO
Game semantics for first-order logic
我们完善HO/N游戏语义的指针（μ指针）的额外概念，并将其扩展到一阶经典逻辑的完整性结果。我们使用一个教堂风格的扩展Parigot的Mu-演算来表示一阶经典逻辑的证明。我们提出了一些关系Krivine的经典的可实现性和应用类型同构。
2010-10-20 cs.LO
Graded Hoare Logic and its Categorical Semantics
基于程序逻辑的演绎验证技术（即，Floyd-霍尔逻辑族）是用于程序推理的强大方法。最近，有一种趋势是增加这种逻辑的表达能力，通过增加额外的信息来推断程序的副作用。例如，一般的程序逻辑已经增加了成本分析，逻辑的概率计算已经增加了估计措施，和逻辑的差分隐私与不可否认的界限。在这项工作中，我们统一这些不同的方法，通过分级的范例，适应世界的功能演算和语义。我们提出了分级霍尔逻辑（GHL），一个参数化的框架，用于增强程序逻辑与一个预序monoidal分析。我们开发了一个语义框架GHL建模，使分级，逻辑断言（前和后条件）和潜在的有效语义的命令式语言可以集成在一起。我们的框架的核心是一个分级的范畴，我们在这里扩展的概念，引入分级Freyd类别，提供了一个语义，可以解释许多例子，从文献中的增强程序逻辑。我们利用相干纤维化来建模基本断言语言，因此整体设置也是纤维化的。
2021-01-26 cs.LO
Graph-based Interpretation of Normal Logic Programs
在本文中，我们提出了一个依赖图为基础的方法来计算正常的逻辑程序的各种语义。我们的方法采用\textit{conjunction nodes}明确表示正常的逻辑程序的依赖图。该依赖图可以以语义保持的方式进行适当的转换，并重新转换为等价的正常逻辑程序。这种转换后的正规逻辑程序可以用回答集编程（ASP）中编写的一些规则来扩充，并使用CLINGO系统来计算其回答集。根据这些附加规则在ASP中的编码方式，可以在稳定模型语义、良基语义或共稳定模型语义下计算原始正常逻辑程序的模型。在每种情况下，也会生成模型中每个原子的对齐。我们报告我们的方法的实施以及其性能评估。
2021-11-25 cs.LO
A lemma on closures and its application to modularity in logic programming semantics
本文指出了单调增函数闭包的一个引理，并说明了它如何适用于定义为某个单调函数的最小不动点的语义的分解和模性。特别地，它适用于逻辑程序的许多语义。一个附录解决了夹在具有相同不动点的函数之间的（可能是非单调的）函数的不动点。
2020-08-03 cs.LO
Bialgebraic Semantics for Logic Programming
双代数提供了一个抽象框架，包含不同类型的计算模型的语义。在本文中，我们提出了一个双代数方法的语义逻辑程序设计。我们的方法是研究逻辑程序作为反应系统，并利用抽象技术开发的设置。首先，我们使用饱和度模型的操作语义的逻辑程序作为余代数上的预层。然后，利用预层上的双代数，明确了其代数结构。由此产生的语义原来是组合方面的连接和长期替代。此外，它还编码了一个并行计算模型，其可靠性由不同线程之间的内置同步概念保证。
2015-03-27 cs.LO
Virtual Evidence: A Constructive Semantics for Classical Logics
本文提出了一个计算语义的经典逻辑使用建设性类型论。这样的语义似乎是不可能的，因为经典逻辑允许排中律（LEM），而在构造性逻辑中不被接受，因为它没有计算意义。然而，在逻辑推理模型中所表达的明显的神谕力量，即对于任何命题P，要么它是真的，要么它的否定是真的，而不是P，也可以用不涉及“真理的神谕”的构造性证据来解释。具有虚拟证据和否定证据的构造性不可能性的类型为经典真理提供了足够的语义基础，并且具有简单的计算意义。这个想法是使用精化类型形式化的，精化类型是自1984年以来使用的构造性类型论的概念，在这里解释。一个新的公理创建虚拟证据，充分保留了经典语境中的逻辑算子的建设性意义。关键词：经典逻辑，构造性逻辑，直觉主义逻辑，命题类型，构造性类型论，精化类型，双重否定翻译，计算内容，虚拟证据
2014-08-31 cs.LO
Intuitionistic computability logic
可计算性逻辑（Computability Logic，CL）是关于计算任务和资源的系统形式化理论，在某种意义上，它可以被看作是线性逻辑的一种基于语义的替代。凭借其富有表现力和灵活的语言，其中公式表示计算问题，“真理”被理解为算法可解性，CL可能为建设性应用理论和计算系统提供全面的逻辑基础，这些理论和系统本质上需要建设性和计算意义的底层逻辑。其中最著名的构造主义逻辑是海廷的直觉演算INT，其语言可以被看作是CL语言的一个特殊片段。然而，INT的建构主义哲学从来没有真正找到一个直观上令人信服的和数学上严格的语义证明。CL有很好的索赔提供这样一个理由，因此实现了哥洛夫的著名论文“INT =逻辑问题”。本文包含了一个可靠性证明INT的CL语义。有关CL的全面在线资源，请访问http://www.cis.upenn.edu/~giorgi/cl.html
2006-06-14 cs.AI cs.LO math.LO
