A continuum of incomplete intermediate logics
Tadeusz Litak
本文推广了V.B. Shehtman提出了第一个Kripke不完全中介逻辑，给出了这种逻辑的连续统。这个版本修正了我在Shehtman原始逻辑的不完整性的简化证明中的一个错误。
This paper generalizes the 1977 paper of V.B. Shehtman, which constructed the first Kripke incomplete intermediate logic, by presenting a continuum of such logics. This version fixes an error in my simplified proof of incompleteness of Shehtman's original logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
First-order logic with incomplete information
我们开发了一阶逻辑和一些扩展不完全信息的情况下，并考虑相关的复杂性问题。
Semantic Incompleteness of Liberman et al. (2020)'s Hilbert-style System for Term-modal Logic K with Equality and Non-rigid Terms
本文证明Liberman等人（2020）针对带等词与非刚性项的项模态逻辑K提出的希尔伯特式系统语义不完备，并通过引入使常元和函数符号含义相对化的非标准克里普克语义给出反例。
Mechanizing Gödel's Incompleteness Theorems and Provability Logic
该研究在Lean 4中形式化验证了哥德尔不完备定理及可证性逻辑GL的Solovay完备性，为数学基础提供机器证明。
Two Fuzzy Logic Programming Paradoxes Imply Continuum Hypothesis="False" & Axiom of Choice="False" Imply ZFC is Inconsistent
提出了[29]中模糊逻辑规划系统的两个不同的悖论。第一个悖论是由于两个不同的（矛盾的）真值为每个基础原子的FLP，一个是语法，另一个是语义。第二个悖论涉及的基数的有效FLP公式，发现有矛盾的值：既$\aleph_0$的基数的自然数，和$c$，基数的连续。结果是CH=“False”，选择公理=“False”。因此，ZFC不一致。
An epistemic logic for modeling decisions in the context of incomplete knowledge
针对现有决策建模形式化体系无法捕捉不完备知识下决策认知本质的问题，提出结合分层、自认知逻辑与定义的新建模语言，构建层级认知理论知识库以支持认知推理与决策。
A new viewpoint of the Gödel's incompleteness theorem and its applications
本文对哥德尔不完备性定理提出了一个新的观点，揭示了逻辑与计算之间的深层关系。在此基础上，给出了从有限个具体实例中搜索一阶逻辑命题证明的算法，并提出了一种改进神经网络搜索数学证明的方法。
A New Representation Theorem for Many-valued Modal Logics
本文提出了一种新的多值逻辑表示定理的定义，并引入了模态算子，定义了给定逻辑的代数模型与用于定义其Kripke可能世界语义的关系结构之间的更强关系，这种新的框架为基于真值不变性蕴涵的多值逻辑提供了一种新的语义.因此，它与基于具有指定逻辑值子集的矩阵的当前定义有很大不同，用于满足关系，通常难以确定。当多值模态逻辑是基于真值集的完备分配格时，我们得到了一个紧凑的自指Kripke式正则表示。模态逻辑的这个子类的克里普克式语义将多值代数的载体集的联合不可约子集作为可能世界的集合。这个子类的一个重要成员是由新的逻辑值扩展的次协调模糊逻辑，以便也处理不完整和不一致的信息。这个新的理论适用于自认知直觉主义多值逻辑的情况下，基于贝尔纳普的4值双格，作为一个最小的扩展经典逻辑用于管理不完整和不一致的信息以及。
Alternating-time temporal logic with finite-memory strategies
不完全信息的交替时序逻辑ATL和ATL* 的模型检查对于完美召回语义是不可判定的。然而，当限制到无记忆策略的模型检查问题变得可判定。在本文中，我们考虑其他两种类型的语义有限记忆策略的基础上。一种是允许的内存大小有界，另一种是内存大小无界（但必须是有限的）。这是由具有完美召回语义的模型检查的高复杂性和无记忆策略的严重限制所激发的。我们表明，这两种类型的语义介绍是不同的完美召回和无记忆语义和下一个重点的可判定性和复杂性的模型检查在完整和不完整的信息游戏ATL/ATL*。特别是，我们证明了模型检测的复杂性与有界记忆语义是Delta_2 p-完全的ATL和PSPACE-完全的ATL* 在不完全信息的游戏，就像在无记忆的情况下。我们还提出了一个证明，ATL和ATL* 模型检查是不可判定的n >= 3的球员与有限记忆语义的不完全信息游戏。
Incompleteness of States w.r.t. Traces in Model Checking
Cousot和Cousot介绍并研究了一种通用的过去/未来时间规约语言，称为mu *-演算，具有自然的时间对称的基于迹的语义。mu *-演算的标准的基于状态的语义是其基于迹的语义的抽象解释，这被证明是不完整的（即，不完整的轨迹），即使是有限的系统。因此，标准的基于状态的模型检验的μ * 演算是不完整的w.r.t.基于轨迹的模型检验。本文表明，任何细化或抽象域的状态集诱导相应的语义仍然是跟踪不完整的任何命题片段的μ * 演算。这是从许多结果中得出的，每个结果对应于mu * 演算的不完整逻辑/时间连接符，这些结果表征模型的结构，即转换系统，其对应的mu * 演算的基于状态的语义是迹完备的。
ATLsc with partial observation
交替时间时态逻辑与策略上下文（ATLsc）是一个强大的形式主义表示多智能体系统的属性：它扩展了CTL与策略量词，提供了一个方便的方式来表达多个代理之间的合作和对抗。状态空间的不完全观测是这种框架中的一个理想特征，但它很快会导致不可判定的验证问题。在本文中，我们证明了均匀的不完全观察（其中所有玩家都有相同的观察）保留了模型检查问题的可判定性，即使是非常有表现力的逻辑，如ATLSC。
Probabilistic Model Checking of Incomplete Models
为了保证模型检验的准确性，模型必须是系统的完整和忠实的表示。不幸的是，这并不总是可能的，主要是因为两个原因：（i）模型仍在开发中，（ii）一些模块的正确执行尚未确定。在这样的情况下，对于某些模型检验查询，是否仍然可能得到正确的答案？本文是回答这个问题的一个步骤。我们制定这个问题的离散时间马尔可夫链（DTMC）建模形式主义和概率计算树逻辑（PCTL）查询语言。然后，我们提出了一个简单的解决方案，通过修改DTMC和PCTL，以适应三值逻辑。该技术建立在现有的模型检验算法和工具，避免了需要新的占三值逻辑。对复杂系统建模的最有用和最流行的技术之一是通过离散事件仿真。离散事件模拟器本质上是用某种程序设计语言编写的代码。我们展示了我们的方法在一段代码中的应用，其中包含一个未知的正确性模块。本文的初步版本出现在Leavering Applications of Formal Methods，Verification and Validation：Foundational Techniques（ISoLA 2016），LNCS 9952，Springer的会议录中。关键词：概率模型，概率模型检验三值逻辑，离散时间马尔可夫链，概率计算树逻辑。
Semantics for Possibilistic Disjunctive Programs
本文定义了一种用于不确定、不完全和不一致信息建模的可能性析取逻辑规划方法。该方法引入了可能性选言分句的使用，它能够同时捕获知识库的不完整信息和不完整状态。将可能性逻辑程序看作是一种可能性逻辑理论，定义了一种基于回答集和可能性逻辑证明理论的可能性逻辑程序设计语义的构造方法.它表明，这种可能性语义的析取逻辑程序可以表征为一个不动点算子。它还表明，建议的可能性语义可以计算的决议算法和考虑最佳反驳从可能性逻辑理论。为了管理不一致的可能性逻辑程序，定义了不一致可能性模型间的偏好准则，并采用割集方法恢复不一致可能性知识库的一致性.该方法是在一个医疗场景中说明。
A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic
本文比较可归约性语义与基语义（含Sandqvist变体）三种单调证明论语义，建立二者间的转换条件，并据此讨论直觉主义逻辑的基完备性问题。
Interpolation in Linear Logic and Related Systems
本文证明了带交换的完整Lambek演算及经典与直觉线性逻辑等存在连续统多个具有演绎插值性质的公理扩张，并指出它们虽不具备Craig插值性质，但均满足受守卫形式的Craig插值。
Characteristic formulas over intermediate logics
将特征公式的概念推广到无限可表示的亚直不可约代数。证明了Heyting代数簇的连续统中含有无限个可表示的次直不可约代数。此外，我们证明了存在一个连续的中间逻辑，可以公理化的特征公式的无限代数，而它们是不可公理化的标准Jankov公式。给出了不能用无限代数的特征公式公理化的中间逻辑的例子。同时，利用Goedel-McKinsey-Tarski变换，我们将这些结果推广到了S4的内部代数和正规扩张
Combining fragments of classical logic: When are interaction principles needed?
我们研究了经典逻辑片段的组合，作为通过添加新的连接词来保守扩展给定布尔逻辑的一种方式，并且我们精确地描述了这样的组合在包含来自两个片段的连接词的签名上产生相应的经典逻辑片段的情况。作为输入。如果由此产生的组合片段只是不完全地被作为输入的成分所表征，这意味着来自一个成分的连接词需要与来自另一个成分的连接词相互作用，从而产生相互作用原则。主要的贡献强烈依赖于（众所周知的）描述的2值克隆后，（不那么知名）公理化程序的2值矩阵奠定了劳滕贝格，并对阿夫隆的非确定性矩阵，这已（最近）被用来产生一个显着的进步理解的语义fibring。
Invariant Synthesis for Incomplete Verification Engines
我们提出了一个框架，综合归纳不变量不完整的验证引擎，健全的逻辑问题，在不可判定的理论，可判定的理论。我们的框架是基于反例引导归纳合成原理（CEGIS），并允许验证引擎沟通非证明性信息，以指导不变的合成。我们精确地展示了验证引擎如何计算这种非可证明性信息，以及如何构建有效的学习算法时，不变量表示为一组固定的谓词的布尔组合。此外，我们评估我们的框架中的两个验证设置，一个是验证引擎需要处理量化的公式，一个是验证引擎必须对堆属性的原因表示在一个富有表现力的，但不可判定的分离逻辑。我们的实验表明，我们的不变量合成框架的基础上的不可证明性信息，可以有效地合成归纳不变量，并充分加强合同在一个大的程序套件。
Skolemization In Intermediate Logics
本文刻画了允许标准及Andrews Skolem化的中间一阶逻辑，并为其他逻辑开发新型Skolem函数，同时证明带量词移位公理的谓词直觉主义逻辑的Kripke框架不完全性，以促进非经典逻辑的消解式定理证明。
On an ordinary expansion of first-order Belnap-Dunn logic
本文提出了一种第一阶Belnap-Dunn逻辑的扩展，通过经典逻辑等价律区分其与其他逻辑，并探讨其在处理归纳机器学习中的不一致和不完整性方面的潜力。
Universal Algebra and Mathematical Logic
本文在泛代数的框架内，利用在前三篇论文中发展起来的克隆理论，解释了一阶逻辑。我们首先定义一个一阶语言L的项在参数集C上的自由克隆T（L，C）。T（L，C）上公式的自由右代数F（L，C）则由原子公式生成。C上L的结构表示为F（L，C）的完美赋值，而L的理论表示为F（L）的滤子。最后，如预期的那样陈述了哥德尔完备性定理和第一不完备性定理。
Non-finite axiomatizability of Dynamic Topological Logic
动态拓扑逻辑（DTL）是一种多模态逻辑，用于对{ \em}动态拓扑系统进行推理。它们是对（X，f），其中X是拓扑空间，f：X->X是连续的。DTL使用一种语言L，它将拓扑S4模态[]与线性时态逻辑中的时态运算符结合起来。最近，我给出了一个声音和完整的公理化DTL* 的逻辑语言L* 的扩展，其中<>被允许作用于有限的公式集，并被解释为一个纠结的封闭运算符。没有完整的公理化是已知的L上，虽然一个证明系统，我们将称为$\mathsf{KM}$，是由克雷默和薄荷糖证明是完整的。本文证明了：给定L和L* 之间的任何语言L'，L'的有效公式集都不是可公理化的.因此，知识管理尤其是不完整的。
Mechanised uniform interpolation for modal logics K, GL, and iSL
本文在 Coq 中机械化计算并证明了模态逻辑 K、GL 和 iSL 的命题量词可定义性（一致插值），完善了 GL 的现有证明，实现了 iSL 的首次证明论构造，并提供了经过验证的计算程序。
Contraction-free proofs and finitary games for Linear Logic
在Girard线性逻辑的标准表示中，有两个前提不小于结论的“非减”规则，即切割规则和收缩规则。废除“一刀切”规则是一个普遍关注的问题。我们表明，使用一个容许的修改张量规则，可以消除收缩，并削减可以同时限制到一个单一的初始发生。这种观点导致一个一致的，但不完整的游戏模型LL指数，这是有限的，在这个意义上说，每个游戏是有限的。该游戏是基于一组推理规则，不享受削减消除。尽管如此，切割规则在模型中仍然有效。
Recursive enumerability and elementary frame definability in predicate modal logic
研究了一阶谓词模态逻辑中递归可枚举性与基本框架可定义性之间的关系。一方面，众所周知，每个一阶谓词模态逻辑关于Kripke框架的基本类完备，即，一类可由经典一阶公式定义的框架是递归可递归的。另一方面，基于本质上具有二阶Kripke语义的“自然”命题模态逻辑的谓词模态逻辑的许多例子是已知的，它们要么不是递归可排数的，要么是Kripke不完全的。这就提出了一个问题，即是否每一个Kripke完备的、递归可判定的谓词模态逻辑都可以用一个Kripke框架的基本类来刻画。我们回答这个问题的否定，通过构建一个正常的谓词模态逻辑，这是Kripke完全的，递归可重复的，但不完全的一个基本类的框架。我们还提出了一个正常的谓词模态逻辑的例子，是递归可重复的，Kripke完全的，不完全的一个基本类的根框架，但相对于一个基本类的框架，没有根是完整的。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。