A temporal logic of epistemic and normative justifications, with an application to the Protagoras paradox
本研究结合带过去与未来模态的线性时态逻辑与道义辩护逻辑，构建含两类辩护断言的推理框架，给出两种语义并证明公理系统的可靠性与完备性，还形式化分析了普罗泰戈拉悖论。
2021-09-21 cs.LO
First-order justification logic with constant domain semantics
证明逻辑是一个术语，用于识别一个相对较新的类模态逻辑家族。有一个既定的文学命题的理由逻辑，但入侵的一阶情况是稀缺的。在本文中，我们提出了一个常数域语义的一阶逻辑证明的Barcan公式（FOLPb），然后我们证明的可靠性和完备性定理。文献中已经有了不含巴坎公式的这种逻辑版本的单调语义，但常数域需要大量的新机制，这可能在其他上下文中也很有用。虽然我们的工作主要是一个系统，我们也表明如何推广这些结果的量化版本的JT 45，对应的模态逻辑S5的理由。我们相信我们的方法更普遍适用，但首先检查具体情况应使工作更容易遵循。
2018-08-29 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
本研究提出一种基于量化认知与证立逻辑的框架，通过非标准同一性处理刻画计算信任的超内涵性，给出证明系统与框架语义并证明可靠性完备性，为计算信任的形式化理论提供逻辑基础。
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
The Complexity of Satisfiability in Non-Iterated and Iterated Probabilistic Logics
设L是经典命题逻辑的某种扩展。L上的非迭代概率逻辑是通过在L语言中添加非嵌套概率算子而定义的逻辑PL。例如，在PL中，我们可以表达这样的陈述“A的真实性概率为0.3”，其中A是L的公式。L上的迭代概率逻辑是逻辑PPL，其中概率运算符可以迭代（嵌套）。例如，在PPL中，我们可以表达这样的语句“这枚硬币是伪造的概率为0.6”。本文研究了概率算子对PL和PPL中可满足性复杂性的影响，得到了上述可满足性问题的复杂性界，该复杂性界是以既没有概率算子也没有经典算子作为顶连接符的正负公式的合取可满足性复杂性为参数的.作为我们的结果的应用，我们得到了紧的复杂性界的可满足性问题在PL和PPL时，L是经典的命题逻辑或理由逻辑。
2019-02-10 cs.CC cs.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
Iterated Belief Base Revision: A Dynamic Epistemic Logic Approach
UFBA（巴西联邦巴伊亚大学）；UFRGS（巴西联邦里约格兰德联邦大学）；PUCRS（巴西天主教里约格兰德大学）
AGM的信念修正是信念改变操作研究的主要范式之一。在这种情况下，信念基地（优先基地）已在很大程度上用于指定代理的信念状态-无论是代表代理的“明确的信念”或作为一个计算模型，她的信念状态。虽然连接的迭代AGM类操作和它们的编码在动态认知逻辑已经研究过，很少有作品考虑如何著名的假设从迭代信念修正理论的特点是通过信念基地和他们的对手在动态认知逻辑。这项工作研究如何优先图，语法表示的偏好关系深深连接到优先基地，可以用来识别信念变化算子，专注于众所周知的假设迭代信念变化。我们提供的句法表示的信念变化运营商在一个动态的背景下，以及新的负面结果的可能性，表示一个迭代的信念修订操作使用优先图上的转换。
2019-02-17 cs.AI cs.LO
Dynamic Preference Logic meets Iterated Belief Change: Representation Results and Postulates Characterization
Federal University of Bahia（巴伊亚联邦大学）；Pontifical Catholic University of Rio Grande do Sul（南里奥格兰德天主教大学）；Federal University of Rio Grande do Sul（南里奥格兰德联邦大学）
AGM的信念修正是信念改变操作研究的主要范式之一。最近，在文献中已经提出了几种用于信念和信息改变的逻辑，并用于在丰富和富有表现力的语义框架中对信念改变操作进行编码。虽然Segerberg的工作已经研究了AGM类操作及其在动态doxastic逻辑中的编码之间的联系，但据我们所知，动态认知逻辑（DEL）领域的大多数工作都没有尝试使用这些逻辑作为工具来研究信念变化算子的数学性质。这项工作研究如何动态偏好逻辑，在DEL家庭的逻辑，可以用来研究动态信念变化算子的属性，重点是众所周知的迭代信念变化的假设。
2021-01-05 cs.AI cs.LO
A Logical Characterization of Iterated Admissibility
Cornell University（康奈尔大学）
Brandenburger，Friedenberg和Keisler提供了迭代可接受性的认识论特征（即，弱劣势策略的迭代删除），其中不确定性使用LPS（词典概率序列）表示。它们的特征在一个称为完整结构的丰富结构中保持，其中所有类型都是可能的。本文给出了迭代容许性的一个逻辑特征，它只涉及标准概率，并且不仅适用于完备结构，而且适用于所有结构。一个更强的概念，强容许性，然后定义。粗略地说，强可容许性是为了捕捉这样一种直觉，即“代理人所知道的一切”是其他代理人满足适当的理性假设。强可容许性使得可容许性、规范结构（典型地在模态逻辑的完备性证明中考虑）、完备结构和“我所知道的一切”的概念之间的关系成为可能。
2009-06-23 cs.AI cs.GT 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
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution
在诸如分离逻辑之类的权限逻辑中，迭代分离合取是表示对堆位置的无界集合的访问权限的量词。与递归谓词相反，迭代分离合取并不规定它们所覆盖的位置的结构，因此不限制如何遍历和修改这些位置。这种灵活性对于验证随机存取数据结构（例如数组）和可以以多种方式遍历的数据结构（例如图形）是重要的。尽管它的有用性，没有自动程序验证原生支持迭代分离合取，他们是特别难以纳入符号执行引擎，流行的技术，为这些逻辑建立验证。在本文中，我们提出了第一个符号执行技术，以支持一般迭代分离合取。我们提出了一种新的表示符号堆和灵活的支持，量化堆位置的逻辑规范。我们的技术表现出可预测的和快速的性能，尽管在SMT级别采用量词，通过仔细控制量词实例。它与权限逻辑的其他功能兼容，如部分权限、递归谓词和抽象函数。我们的技术是实现作为一个扩展的毒蛇验证基础设施。
2016-05-06 cs.LO cs.PL
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
Bringing Belief Base Change into Dynamic Epistemic Logic
Institute of Mathematics and Statistics, Federal University of Bahia - UFBA（巴伊亚联邦大学数学与统计学院）
AGM的信念修正是信念改变操作研究的主要范式之一。在这种情况下，信念基地（优先基地）已主要用于指定代理的信念状态。虽然连接的迭代AGM类操作和他们的编码在动态认知逻辑已经研究过，很少有作品考虑如何著名的假设迭代信念修正理论可以通过信念基地和他们的对应物在动态认知逻辑的特点。特别是，它已被证明，一些假设可以通过优先图中的转换来表征，而其他假设则可能无法以这种方式表示。这项工作研究动态偏好逻辑的语义变化，产生了一个适当的语法表示其模型，使我们能够表示和推理迭代的信念基础变化在这个逻辑。
2019-12-22 cs.AI cs.LO
Tree-Like Justification Systems are Consistent
KU Leuven（鲁汶大学）；Vrije Universiteit Brussel（布鲁塞尔自由大学）
证明理论是一种抽象的统一形式主义，它捕捉了各种非单调逻辑的语义。一个有趣的问题，已收到显着的关注是一致性问题：在何种条件下是一个事实的理由和理由，其否定适当相关。有两种证明理论：一种是证明是树，另一种是证明是图。在这项工作中，我们解决了一致性问题，一劳永逸的树一样的设置显示，所有合理的树一样的理由系统是一致的。
2022-08-05 cs.AI cs.LO
A Logic for Non-Monotone Inductive Definitions
著名的归纳法原理包括单调归纳法和各种非单调归纳法，如膨胀归纳法、良基集上的归纳法和迭代归纳法。在这项工作中，我们定义了一个逻辑形式化归纳良好的基础集和单调和迭代归纳。正如正归纳原理已在FO（LFP）中形式化，膨胀归纳原理已在FO（IFP）中形式化一样，本文在一种新的非单调归纳定义逻辑（ID-逻辑）中形式化了迭代归纳原理。逻辑的语义受到逻辑编程的良基语义的强烈影响。我们的主要结果是关于ID逻辑中归纳定义的模性质。具体而言，我们制定的条件下，同时定义$\D$的几个关系是逻辑上等同于一个连接的较小的定义$\D_1 \land ... \land \D_n$与不相交的定义谓词。这个结果的困难来自这样一个事实，即分别在$\D_i$和$\D_j$中定义的谓词$P_i$和$P_j$可以通过同时归纳相互连接。由于良基语义下的逻辑程序设计和溯因逻辑程序设计是我们的逻辑的适当片段，我们的模块性结果也适用于那里。
2005-01-13 cs.AI cs.LO
A categorical and logical framework for iterated protocols
本文用范畴论重构协议复形方法，证明其函子与自由代数结构，并提出时序—认知逻辑语义，以刻画迭代分布式协议。
2025-05-15 cs.DC cs.LO
A Decidable Class of Nested Iterated Schemata (extended version)
Grenoble University（格勒诺布尔大学）；CNRS（法国国家科学研究中心）
许多问题可以通过依赖于参数的命题公式的模式来指定，例如，电路的规格通常取决于其输入的位数。我们定义了一个逻辑的公式，称为“迭代图式”，允许表达这样的模式。图式用索引命题（如P_i，P_i+1，P_1）和广义连接词（如/i=1）扩展命题逻辑。n或i=1.. n（称为“迭代”），其中n是称为“参数”的（未绑定）整数变量。迭代模式的表达能力严格地大于命题逻辑：它甚至超出了一阶逻辑的范围。我们定义了一个证明过程，称为DPLL*，可以证明一个模式是满足至少一个值的参数，在精神的DPLL过程。然而，相反的问题，即证明模式对于参数的每个值都是不可满足的，是不可判定的，所以DPLL* 一般不会终止。尽管如此，我们证明，它终止的语法子类称为“定期嵌套”的模式。这是第一个非平凡类，DPLL* 被证明终止。此外，规则嵌套模式的类是第一个允许迭代嵌套的可判定类，即允许模式的形式/n =1.。n（/ \j =1.. n.）。
2010-01-24 cs.AI cs.LO
A Game Theoretical Semantics for Logics of Nonsense
无意义逻辑允许第三个真值来表达\emph{nonsense}的命题。这些逻辑是理解程序中如何处理错误以及错误一旦出现如何在整个程序中传播的理想形式。本文给出了无义逻辑的Hintikkan博弈语义，并证明了它的正确性。我们还讨论了如何在博弈论中的一个已知的解决方案的方法，严格劣势策略的迭代消除，涉及到语义游戏的逻辑废话。最后，我们仅用语义游戏的方法扩展了无意义逻辑，发展了一种新的无意义逻辑，并为Priest的Parabel逻辑提出了一种新的游戏语义。
2020-09-23 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
True Lies
University of Bergen（卑尔根大学）；Zhejiang University（浙江大学）；University of Lorraine（洛林大学）；Peking University（北京大学）
一个真正的谎言是一个谎言，当宣布成为真实。在宣告的逻辑中，宣告的代理人没有被建模，真正的谎言是一个公式（它是假的），当宣告时变成真的。我们调查真实的谎言和其他类型的相互作用之间宣布的公式，他们的先决条件和后置条件，在设置Gerbrandy的逻辑相信公告，其中代理人可能有或获得不正确的信念。我们的结果是满足性和有效性的实例化这些语义定义的类别，迭代公告，包括任意经常迭代公告，和句法表征。我们关闭的结果迭代公告的逻辑知识（而不是信仰），并撒谎作为私人公告（而不是公共公告）不同的代理。详细的例子说明了我们说谎的概念。
2017-04-27 cs.AI cs.LO cs.MA
Eigenlogic in the spirit of George Boole
这项工作提出了一个操作和几何方法的逻辑。它从乔治布尔介绍的原始形式的二元逻辑函数的多线性选择分解开始。一个理由的历史理由提出桥接布尔的理论和使用他的算术逻辑功能与公理的布尔代数使用集和量子逻辑。它表明，这种代数多项式制定可以自然地扩展到有限向量空间中的运营商。逻辑运算符将作为交换投影运算符出现，并且取二进制值{0，1}的真值是相应的特征值。在这种观点中，一个逻辑命题的解是由对一个论证组合的运算产生的，它将表现为一个选择，其中的结果只能是一个特征值。这样，命题逻辑可以通过使用选择性的发展在线性代数中形式化，这些发展在这里对应于张量初等投影算子的组合。这项工作的原始和主要动机是在量子信息的新领域的应用，与更传统的量子逻辑方法的差异进行了概述。
2018-02-06 cs.LO math.LO
It ain't necessarily so: Basic sequent systems for negative modalities
我们期待在非经典的否定和相应的调整连接词从模态的观点，在完整的分配格，并应用一个非常一般的机制，以提供足够的分析证明系统的逻辑是基于它们。在通常的模态语义学中定义非经典否定自动地允许人们将等价公式视为同义的，并且对对位规则的全局版本有一个自然的理由。从这个角度来看，我们的研究提供了一个特别有用的环境中，消极模态和他们的同伴可以用来处理不一致和不确定性。在研究了基于任意框架的模态逻辑之后，我们将结果推广到了序列框架、自反框架、函数框架和对称框架。在每一种情况下，我们也调查何时以及如何经典否定可能从而被定义。
2016-06-23 cs.LO
Decidability and Undecidability Results for Propositional Schemata
CNRS（法国国家科学研究中心）
我们定义了一个逻辑的命题公式图式添加到语法的命题逻辑索引命题和迭代连接词范围内的算术变量参数化的区间。可满足性问题是不可判定的，这个新的逻辑，但我们引入了一个非常一般的类的模式，称为有界线性，这个问题变得可判定。这个结果是通过减少到一个特定的类称为定期的模式，我们提供了一个健全的和完整的终止证明过程。这种模式演算允许一个捕获证明模式对应于一个大类的命题逻辑中指定的问题。我们还表明，可满足性问题再次成为不可判定的轻微扩展这一类，从而表明，有界线性模式代表了一个很好的妥协之间的表达性和可判定性。
2014-01-16 cs.AI cs.LO
