Duality for Fitting's Multi-valued Modal logic via bitopology and biVietoris coalgebra
本文通过扩展双拓扑对偶性并调整双Vietoris构造至成对布尔空间范畴，为Fitting多值模态逻辑建立了双拓扑与余代数对偶性，证明了其可靠性与完备性，并确立了Hennessy-Milner性质。
2025-11-01 cs.LO
Many-Valued Modal Logic
本文提出一种基于有限线性序真值集和真值表联结词的多值极小正规模态逻辑，给出矢列演算并证明其可靠性与强完全性，还证明了有限模型性质并讨论其扩张及与多值直觉主义逻辑的关系。
2024-12-31 cs.LO
Finite Automata Based on Quantum Logic and Their Determinization
给出了正交模格值有限自动机的量子子集构造，并证明了正交模格值有限自动机、正交模格值确定性有限自动机和具有空串移动的正交模格值有限自动机之间的等价性.在此基础上，我们研究了正交模格值正则语言上的代数运算，并在量子逻辑的框架下建立了Kleene定理。
2007-12-28 cs.LO
On Transitive modal many-valued logics
本文主要研究由赋值Kripke框架定义的模态逻辑，特别是在某些剩余格上赋值传递Kripke框架的模态逻辑的可计算性和可表示性问题。它表明，一个大家庭的这些逻辑-包括所产生的标准MV和产品代数-产生一个不可判定的后果关系。随后，传递模态Lukasiewicz逻辑的行为进行了比较，它的非传递对应，展示了一些细节有关的可计算性和等价与其他逻辑。最后，我们展示了不可判定性的有效性和局部SAT问题的传递模型时，Delta操作添加到逻辑。
2019-04-02 cs.LO
Propositional dynamic logic for searching games with errors
本文研究了命题动态逻辑的有限值推广及其检验。我们首先介绍了（n+1）-值Kripke模型和相应的语言的基础上的模态扩展的Mukasiewicz多值逻辑。我们说明的定义提供了一个框架，分析的雷尼-乌拉姆搜索游戏的错误。我们的主要结果是（n+1）值Kripke模型理论的公理化。这一结果是通过对最小（n+1）值命题动态逻辑的正则模型的过滤得到的。
2014-01-28 cs.LO
On sufficient conditions for expressibility of constants in the 4-valued extension of the propositional provability logic $GL$
本文考虑著名的命题可证性逻辑$GL$的最简单的非经典扩展$GL4$以及A.库兹涅佐夫发现了$GL$的四值扩张$L\mathfrak{B}_2$中常数可表示的条件，这是作者在1996年的论文中首次提出的。
2013-12-03 cs.LO
HHLPy: Practical Verification of Hybrid Systems using Hoare Logic
我们提出了一个工具，用于验证的混合系统表示的顺序片段的HCSP（混合通信顺序进程）。该工具允许注释HCSP程序与前，后条件，不变量，并证明规则的推理常微分方程。验证条件是根据混合霍尔逻辑的规则从注释中生成的。我们设计了标记和突出显示机制来区分和可视化不同的验证条件。该工具使用Python实现，并具有基于Web的用户界面。我们评估了翻译的Simulink/Stateflow模型和KeYmaera X基准工具的有效性。
2023-02-21 cs.LO
Hypotheses Founded Semantics of Logic Programs for Information Integration in Multi-Valued Logics
我们解决了整合来自不同来源的信息的问题。信息由中央服务器收集的事实组成，并试图使用（a）一组逻辑规则，即逻辑程序，和（b）表示服务器自己的估计的假设来组合。在这样的设置不完整的信息从一个来源或矛盾的信息从不同的来源需要使用多值逻辑程序可以评估和假设可以测试。为了进行这样的活动，我们提出了一个正式的框架，如贝尔纳普的四值逻辑双格的基础上。在这个框架中，我们的工作与类的程序定义的拟合，我们开发了一个理论的信息集成。我们还建立了一个直观的吸引力之间的连接，我们的假设检验机制，一方面，和有理有据的语义和Kripke-Kleene语义的Datatron程序与否定，另一方面。
2001-11-27 cs.LO
Logical Characterizations of Heap Abstractions
形状分析关注的问题，确定“形状不变量”的程序，执行破坏性更新动态分配的存储。在最近的工作中，我们已经展示了如何使用基于3值一阶逻辑的抽象解释进行形状分析。在这项工作中，具体的存储是有限的2值逻辑结构，并且在执行期间可能出现的存储集合使用有限的3值逻辑结构的某个族来表示（保守地）。在本文中，我们展示了如何在形状分析中出现的3值结构可以使用具有传递闭包的一阶逻辑中的公式来表征。我们还定义了一个非标准的（“超赋值”）语义的3值一阶逻辑，比传统的3值语义更精确，并证明了超赋值语义可以有效地实现使用现有的定理证明。
2005-03-16 cs.LO
An Inductive Construction for Many-Valued Coalgebraic Modal Logic
在本文中，我们提出了一个抽象的框架，多值模态逻辑的原子命题和模态算子的解释为谓词提升余代数上的一个endofunctor的集合范畴。它将Pattinson的共形模态逻辑分层方法推广到多值情形。与规范模型构造和过滤的标准技术相比，该方法采用归纳原理来证明逻辑的可靠性、完备性和有限模型性质。因此，我们可以解除对先前方法的限制~ \cite{Lin2022}，该方法要求底层语言必须具有内在化元级真值赋值操作的表达能力。
2022-10-24 cs.LO
On the construction of multi-valued concurrent dynamic logic
动态逻辑是对命令式程序进行推理的强大框架。引入了一个带有并发操作符的扩展[18]来形式化并行运行的程序。在另一个方向上，其他作者提出了一个系统的方法来生成多值命题动态逻辑来推理加权程序[14]。本文介绍了这两个框架相结合，在并发计算中引入不确定性的第一步。在开发的框架中，权重被分配给并行执行的每个分支，导致模糊编程范式固有的（可能的）非对称并行性[21，2]。通过采用这样的方法，得到了一族逻辑，称为多值并发命题动态逻辑（CGDL（A）），参数上的动作格A指定的“权重”的概念分配给程序执行。此外，还讨论了CPDL中某些公理在新的生成逻辑族中的有效性。
2019-11-01 cs.LO
A Real-Valued Modal Logic
本文提出一种实值多值模态逻辑，结合Kripke语义与实数上的格群运算，通过带标签tableau系统获得coNEXPTIME上界，并建立模态-乘法片段的消割sequent演算及扩展阿贝尔逻辑的完备性。
2018-01-22 cs.LO
A note on calculi for non-deterministic many-valued logics
本文提出两个演绎等价的演算（一个基于公理，一个基于推理规则），它们直接源自真值表，并证明了可靠性与强完备性，以及规则演算的切割消去定理。
2022-10-24 cs.LO
MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications
我们介绍MCMAS-SLK，一个基于BDD的模型检查器的验证系统对规格表示在一个新的，认知的战略逻辑的变体。我们给出了规约语言的语法和语义，并介绍了一个标记算法的认知和策略逻辑模态。我们提供的检查器，也可以用于合成代理的策略，使系统满足规格的细节。我们评估的执行效率，通过讨论用餐密码协议和蛋糕切割问题的一个变种所获得的结果。
2014-05-16 cs.LO
Upper-Expectation Bisimilarity and Real-valued Modal Logics
概率非确定性转移系统的互模拟关系的几个概念已被认为是在文献中。我们认为一种新的基于测试的行为等价称为上期望双相似性，并开发其理论使用线性代数和功能分析的标准结果。我们表明，对于广泛的一类系统，我们的新概念与Segala的凸双相似性相吻合。我们开发的表达概率模态μ-演算和一种新的实值模态逻辑的逻辑刻画。我们证明了上期望双相似性是一个同余的过程代数指定的概率GSOS规则格式的广泛的家庭。
2013-10-02 cs.LO
Sheaves and geometric logic and applications to the modular verification of complex systems
在本文中，我们表明，并发系统的状态，转移和行为往往可以建模为一个合适的拓扑空间上的层。在这种情况下，几何逻辑可以用来描述当互连系统时，在全局级别上保留哪些局部属性（即单个系统的属性）。主要应用领域是复杂系统的模块化验证。我们说明的想法，通过一个例子，涉及一个家庭的相互作用的控制器的火车上的铁路轨道。
2008-10-16 cs.LO
Proceedings of the Sixteenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷为 GandALF 2025（第十六届国际游戏、自动机、逻辑与形式化验证研讨会）论文集，旨在汇聚相关领域产学研人员，推动从理论到应用的广泛主题交流与交叉融合。
2025-09-16 cs.LO
(Metric) Bisimulation Games and Real-Valued Modal Logics for Coalgebras
行为等价可以通过互模拟、模态逻辑和破坏者-防御者博弈来表征。在本文中，我们回顾了这三个角度在一个coalgebraic设置，这使我们能够概括从特定的分支类型的过渡系统。我们感兴趣的定性概念（经典互模拟）以及定量概念（互模拟度量）。我们的第一个贡献是在经典的情况下，介绍了一个破坏者-防御者互模拟游戏的余代数。其次，我们介绍了这种游戏的度量的情况下，并进一步定义了一个实值模态共代数逻辑，从中我们可以得出的策略的扰流板。对于这个逻辑，我们展示了Hennessy-Milner定理的一个定量版本。
2021-04-19 cs.LO
Specification and verification of a linear-time logic for graph transformation
提出一种基于对应物范式的一阶线性时间时序逻辑，用于推理有向图演化，并引入正规范形式简化验证，通过Agda形式化验证其语法与语义。
2023-05-05 cs.LO
Soundness and Completeness of the NRB Verification Logic
这篇简短的论文给出了一个模型，并证明了确定性命令式程序的NRB验证逻辑的完整性，该逻辑在过去曾被用作大型，快速变化的开源C代码档案（如Linux内核源代码）的自动语义检查的基础。该模型是一个彩色的状态转换模型，从上面的一组可能的程序的过渡近似。相应地，逻辑捕获可能在程序中的给定点触发特定缺陷的所有跟踪，但也可能标记误报。
2013-08-18 cs.LO
Finitely-valued propositional dynamic logic
我们研究了命题动态逻辑的一个多值推广，其中Kripke模型的状态公式和状态之间的可达性关系在有限FL-代数中求值。对这个框架的一个自然的解释是关于执行结构化行动的成本的推理。证明了有限FL-代数上的PDL是可判定的。我们还建立了一类基于具有典型常数的交换积分FL-代数的PDL的一般完备性结果。
2020-12-22 cs.LO
Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)
有界验证已被证明是有用的，以检测错误，并增加在程序的正确性的信心。与无界验证相比，通过（有界）内联进行调用和通过（有界）展开进行循环的推理不需要方法规范和循环不变式，因此将注释开销降低到最低限度，即要验证的属性的规范。对于基于传统程序逻辑的验证器，通过内联（和展开）来保存验证：成功的程序w.r.t.某些注释意味着内联程序的成功验证。也就是说，在内联程序中检测到的任何错误都揭示了原始程序中的真正错误。但是，这个基本属性可能不适用于自动分离逻辑验证器，如Caper、GRASShopper、RefinedC、Steel、VeriFast和基于Viper的验证器。在这种情况下，内联通常会更改方法执行所拥有的资源，这可能会影响自动证明搜索算法并引入虚假错误。在本文中，我们提出了第一种技术，验证保持内联自动分离逻辑验证。我们确定了一个语义条件的程序，并证明在Isabelle/HOL，它确保了验证保持内联的最先进的自动分离逻辑验证。我们还证明了一个双重结果：成功验证的内联程序，确保有方法和循环注释，使验证的原始程序有界执行。为了自动检查我们的语义条件，我们提出了两个近似，可以检查语法和程序验证器，分别。我们实现这些检查毒蛇，并证明他们是有效的非平凡的例子，从不同的验证。
2023-03-13 cs.LO
Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
该研究提出渐进精确逻辑，通过新的渐进验证定义和精确逻辑渐进化，统一霍尔逻辑、不正确性逻辑与渐进验证，为同时开发验证、错误查找工具提供基础。
2024-11-30 cs.LO cs.PL
Uniform Cut-free Bisequent Calculi for Three-valued Logics
本文利用双矢列演算BSC统一形式化多种三值逻辑，并构造性证明所得系统无切、具子公式性质且常可推出插值定理。
2024-12-02 cs.LO
An algebraic study of the first order version of some implicational fragments of the three-valued Lukasiewicz logic
MV-代数是Lukasiewicz逻辑的代数语义，由有限链生成的MV-代数是Heyting代数，其中Godel蕴涵可以用De Morgan和Moisil的模态算子表示。在我们的工作中，三价Lukasiewicz逻辑的一个片段进行了研究。提出了命题逻辑和一阶逻辑。在这两种情况下，极大相容理论被研究为Lindenbaum-Tarski代数的Monteiro极大演绎系统。从而证明了关于适当代数结构的充分性定理。
2020-10-23 cs.LO
An Experiment of Randomized Hints on an Axiom of Infinite-Valued Lukasiewicz Logic
本文给出了一个由无穷值Lukasiewicz逻辑的公理（1）（2）（3）（4）得到公理（5）的自动推理随机提示策略的实验。在实验中，我们随机生成了一组大小从30到60不等的提示，用于指导定理证明器OTTER进行基于超分辨率的搜索。我们成功地在150 * 6个提示列表中找到了最有用的提示列表（包含30个子句）。此外，我们讨论了一个奇怪的非线性增长的生成子句推导公理（5）通过应用我们的随机提示策略。
2022-04-15 cs.LO
Proceedings of Second International Symposium on Games, Automata, Logics and Formal Verification
本卷包含了第二届游戏、自动机、语言和形式化验证国际研讨会（GandALF 2011）的论文集。会议于2011年6月15日至17日在意大利阿马尔菲海岸的米诺里举行。Gandalf研讨会的目的是为来自不同领域和不同背景的研究人员提供一个论坛，这些研究人员在博弈论，数理逻辑，自动机理论及其在复杂系统的规范，设计和验证中的应用方面有着共同的兴趣。本论文集包含三个特邀演讲和十九篇定期论文的摘要，这些论文是根据原创性、质量和与研讨会主题的相关性通过严格的审查过程选出的。
2011-06-04 cs.LO
Operational semantics and program verification using many-sorted hybrid modal logic
Faculty of Mathematics and Computer Science, University of Bucharest（布加勒斯特大学数学与计算机科学学院）
本文提出基于多类型混合模态逻辑的框架，用于描述编程语言操作语义并验证程序正确性，相较于传统方法具有更自然的执行描述和更清晰的语义编码。
2025-11-27 cs.LO
Encoding many-valued logic in $λ$-calculus
本文扩展Church编码至McCarthy三值逻辑，并推广到四、五值逻辑，在无穷λ-演算中通过⊥统一不可解项，还适用于λI-演算，并用于计算无限命题真值以探讨Russell悖论。
2021-06-26 cs.LO
Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
本文针对可实例化于多类车站的通用联锁逻辑，结合 Dafny 编码、模板不变式与参数化模型检验器生成的不变式，实现关键安全性质的自动化参数化验证。
2024-02-29 cs.LO
Temporal Runtime Verification using Monadic Difference Logic
在本文中，我们提出了一个算法进行运行时验证的有界时序逻辑超过定时运行。该算法由三个要素组成。首先，将待验证的有界时态公式转化为差分不等式上的一元一阶逻辑，我们称之为一元差分逻辑。其次，在定时运行的每一步，通过计算与该步的状态和时间的商来修改一元差分公式。第三，通过一元差分逻辑的判定过程来检验所得到的公式是重言式还是不可满足的。基于数据结构差分决策图，我们进一步给出了一元差分逻辑的简单决策过程。该算法是完备的，在一个非常强的意义上的一个子类的时间公式的特点是均匀monadic和它是近似的其他公式。近似值来自于这样一个事实，即并非所有不可满足或重言式公式都能在运行时验证的尽可能早的时间被识别。与现有的方法相反，所提出的算法不工作的语法重写，但采用有效的决策结构，使它们适用于在实际应用中，例如商业软件。
2007-05-31 cs.LO
External Behavior of a Logic Program and Verification of Refactoring
本文为一种简单回答集编程语言精确定义外部行为，并提出一个证明助手来验证程序重构的正确性。
2023-05-27 cs.LO
Four imprints of Belnap's useful four-valued logic in computer science
本文回顾了理论计算机科学中与Belnap四值逻辑相关的四个领域，指出其影响通过双格的扭曲积表示体现，尤其在d-框架、线性逻辑和Blame演算中。
2025-03-26 cs.LO
Symbolic QED Pre-silicon Verification for Automotive Microcontroller Cores: Industrial Case Study
我们提出了一个工业案例研究，证明了实用性和有效性的符号快速错误检测（符号QED）在检测逻辑设计缺陷（逻辑错误）在预硅验证。我们的研究重点是几个微控制器核心设计（约1，800个触发器，约70，000个逻辑门），这些设计已经使用工业验证流程进行了广泛验证，并用于各种商业汽车产品。研究结果如下：1.符号QED检测到了工业验证流程（包括各种基于模拟的验证和形式化验证）检测到的设计中的所有逻辑错误。2.符号QED检测到工业验证流程未记录的其他逻辑错误。（这些额外的错误也可能被工业验证流程检测到。3.符号QED能够显著提高设计生产率：（a）提高8倍（即，减少）验证工作量（符号QED为8人-周，而使用工业验证流程为17人-月）。(b)后续设计的验证工作量提高了60倍（符号QED为2人日，而使用工业验证流程为4-7人月）。(c)快速错误检测（运行时间为20秒或更短），以及用于快速调试的短反例（10条或更少指令），使用符号QED。
2019-02-04 cs.LO
Scope Logic: Extending Hoare Logic for Pointer Program Verification
本文提出了一种扩展霍尔逻辑的指针程序验证方法。首先，对VDM使用的部分函数逻辑（LPF）进行扩展，以指定使用指针的存储器访问和复合类型的存储器布局。然后，本文介绍了数据检索函数（DRF）和内存作用域函数（MSF）的概念。人们可以定义DRF来从互连的具体数据对象中检索抽象值。DRF的对应MSF的定义可以从DRF的定义在语法上导出。这个MSF计算当DRF检索抽象值时访问的内存单元集。这个内存单元集称为抽象值的内存范围。最后，对Hoare逻辑中赋值语句的证明规则进行了修改，使之适用于指针。其基本思想是，只要其作用域中没有内存单元被重写，虚值就保持不变。另一个证明规则是为内存分配语句添加的。结果规则和控制流语句的规则略有修改。它们与霍尔逻辑中的原始版本基本相同。一个例子来显示这种逻辑的有效性。并给出了指针程序验证的一些技巧。
2009-12-21 cs.LO
On Three-Valued Modal Logics: from a Four-Valued Perspective
本文旨在以生动的直观形象、令人信服的哲学论证和广泛的实际应用，全面解决三值模态逻辑的语义定义这一古老的开放性问题。本文在已有的从创新的角度研究三值逻辑的基础上，采用迂回的方法从四值的角度解释三值逻辑，从而为三值模态逻辑的开发、解释和应用提供了一个通用的、系统的方法论。我们通过两个具体的例子来说明我们的方法，一个是道义的，另一个是认识的，对于这两个声音和强完整的自然演绎证明系统也详细介绍。我们认为，我们的三值模态逻辑作为一个轻量级的候选人合并道义或认知的概念到时态逻辑，没有更重的负担，多模态。
2022-09-27 cs.LO math.LO
Neutrality and Many-Valued Logics
在这本书中，我们考虑各种多值逻辑：标准，线性，双曲，抛物，非阿基米德，p-adic，区间，代数等，我们还调查的结果，显示树不同的证明理论框架的多值逻辑，例如框架的下列演绎演算：希尔伯特的风格，代数，和hyperados。我们提出了一个一般的方法，允许系统地构建一个大家庭的非阿基米德多值逻辑分析演算：超有理值，超实值，和p-adic值逻辑的特点是一个特殊的格式的语义与适当的拒绝阿基米德公理。这些逻辑是作为标准多值逻辑（即Lukasiewicz逻辑、Goedel逻辑、Product逻辑和Post逻辑）的不同扩展而构建的。阿基米德公理的非正式意义是任何东西都可以用尺子测量。没有阿基米德公理的逻辑多重有效性也在于真值的集合是无限的，它不是良基的和良序的。在非阿基米德值逻辑的基础上，我们构造了非阿基米德值区间代数逻辑INL，用它来描述中性现象。
2007-07-21 cs.AI cs.LO
Automatic Generation of Proof Tactics for Finite-Valued Logics
现在有许多灵活的基于策略的逻辑框架，它们可以使用一种通用的高阶元语言来实现广泛的数学理论。作为证明助手，这种强大的系统的优点之一在于它们对推理能力的可扩展性的响应，其设计基于规则的程序设计语言，允许用户构建自己的“程序来构造证明”--所谓的证明策略。本贡献讨论了实现的算法，产生声音和完整的画面系统的一个非常包容的类充分表达有限值命题逻辑，然后说明了一些挑战和困难的算法形成的自动定理证明策略，这样的逻辑。我们将报告其实现的过程是基于证明系统的分析性的广义概念，旨在保证终止相应的自动化策略，这些策略涉及我们目标逻辑中的定理。
2010-03-25 cs.LO
Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics
本文是一个贡献的理论基础和有效的自动化证明程序的非经典逻辑的实际建设。我们在这里集中在有限值逻辑的情况下，并展示：（i）一种机制，用于产生一个类似经典的描述，他们在一个有效的各种二价语义;（ii）用于从如此获得的二价语义中提取均匀（classically-labeled）cut-免费的标准分析表格与可能的分支可逆规则，并与证明策略配对，旨在保证终止的相关的证明程序;（iii）一种机制，也提供了相同的逻辑，统一的削减为基础的表系统与线性规则。后者的表系统被证明是足够的，即使限制到分析削减，他们也被证明多项式模拟真值表，一个功能，是不享有的前标准类型的表系统（甚至在2值的情况下）。结果是基于有用的概括的概念的分析性和组合性，并说明了一个理论，适用于许多其他类别的非经典逻辑。
2014-08-16 cs.LO
A Formal Framework for Noisy Runtime Verification
Rensselaer Polytechnic Institute（伦斯勒理工学院）；Kansas State University（堪萨斯州立大学）；Tohoku University（东北大学）
本文提出认识动态逻辑EDMon，用于形式化建模噪声运行时验证中的可监控性，并证明其能捕捉文献中众多结果，梳理了与邻近逻辑的关系及定理类。
2026-09-10 cs.LO
Reduction of Many-valued into Two-valued Modal Logics
本文将多值逻辑的二值约简推广到二值多模态逻辑。这种方法是基于多值逻辑的上下文化，引入高阶Herbrand解释类型，其中我们明确地引入了一组代数真值的原始多值逻辑，转换为参数（或可能的世界），和一组经典的两个逻辑值的共存。这种方法接近于注释逻辑中使用的方法，但提供了使用基于Herbrand解释的标准语义的可能性。此外，它使用高阶Herbrand类型的性质，因为它们的基本性质是基于自指Kripke语义，其中可能世界是原始多值逻辑的代数真值。这种自指Kripke语义可以将高阶Herbrand解释扁平化为普通的2-值Herbrand解释，使我们更清楚地了解多值和2-值多模态逻辑之间的关系。该方法被应用于多值逻辑程序类，其中的约简是基于原始多值逻辑的逻辑结构（逻辑连接词）以结构化的方式完成的。在此之后，我们推广的减少一般结构多值逻辑，在一个抽象的方式，基于Suszko的非正式的非建设性的想法。在所有情况下，利用扩展的2值约简，我们得到一类非真值模态元逻辑，其中二值公式是通过对原多值公式应用特定的模态算子而得到的模态语句.
2011-03-04 cs.IT cs.LO math.IT
On Three-Valued Dependence-Like Logics
University of Lodz（罗兹大学）
本文探讨依赖逻辑与三值逻辑的关联，提出两种结合经典联结词与传染性联结词的三值依赖类逻辑，并给出相应的可靠完备无切割二叉相继式演算。
2026-10-07 cs.LO math.LO
Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems
我们认为时间逻辑验证（可能是非线性的）动态系统在连续的状态空间。我们的方法结合了基于自动机的验证和所谓的屏障证书的使用。基于自动机的验证允许将验证任务分解为连续状态空间上的有限的简单约束集合。反过来，这些约束的满足可以（可能是保守的）通过适当构造的屏障证书来证明。因此，我们的方法，再加上基于优化的搜索屏障证书，允许计算验证的动态系统对时间逻辑属性，同时避免显式抽象的动力学通常在文献中做。
2014-03-14 cs.FL cs.LO
Some Closed Classes of Three-Valued Logic Generated by Periodic Symmetric Functions
考虑了由周期对称函数生成的三值逻辑的闭类，这些周期对称函数在来自$\{1,2\}^n$的元组中等于$1$，在其余元组中等于$0$.得到了该类的基存在性和有限基存在性的判别准则。
2016-04-15 cs.LO math.LO
Temporal Many-valued Conditional Logics: a Preliminary Report
Università della Calabria（卡拉布里亚大学）；Università del Piemonte Orientale（东皮埃蒙特大学）
该研究提出多值时态条件逻辑，将含典型性的多值逻辑与LTL时态算子结合以刻画系统动态性，并探索了其在渐进式论证中的实例化应用。
2024-09-06 cs.AI cs.LO
Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第六届国际游戏、自动机、逻辑和形式化验证研讨会（GandALF 2015）的会议记录。研讨会于2015年9月21日和22日在意大利热那亚举行。专题讨论会的会议记录载有三次应邀演讲的摘要和13篇论文，这些论文是经过仔细评估后被接受在会议上介绍的。被接受的论文的主题包括算法博弈论，自动机理论，形式化验证，模态和时序逻辑。
2015-09-23 cs.FL cs.LO
Two principles in many-valued logic
经典上，两个命题在相同的逻辑赋值下为真时，它们恰好是逻辑等值的。此外，两个逻辑赋值是不同的，当且仅当存在一个公式，根据一个赋值为真，而根据另一个赋值为假。实值逻辑是指Petr Hájek意义下的多值逻辑，它关于由[0，1]上的连续三角范数给出的BL-代数的真假值的子代数是完备的。从经典逻辑中抽象出上述两个性质，使我们得到实值逻辑可能满足也可能不满足的两个原则。我们证明了这两个原则是充分的，以扩展的范围内，以消除ukasiewicz和哥德尔逻辑。我们还证明了，在[0，1]的欧几里德拓扑中真假值的集合是闭的这一附加假设下，这两个原则也提供了乘积逻辑的一个特征。
2013-10-09 cs.LO math.LO
The logical content of triangular bases of fuzzy sets in Łukasiewicz infinite-valued logic
继续追求一个研究方向，我们已经探索了与哥德尔-达米特逻辑和Ruspini分区，我们在这里表明，Rukasiewicz逻辑是能够表达的概念，伪三角基的模糊集，一个温和的削弱标准概念的三角基。途中我们的主要结果，我们得到了一个基本的，逻辑独立的特征的三角基地的模糊集。
2012-10-31 cs.LO math.LO
From Matching Logic To Parallel Imperative Language Verification
程序验证是开发程序的证明系统，并证明证明系统相对于程序的可信操作语义的可靠性。然而，许多实用的程序验证器不是基于操作语义的，不能认真验证程序。提出了基于匹配逻辑的操作语义程序验证方法。本文在Grigore Ro{n}u的工作基础上，研究了并行命令式语言（PIMP）的匹配逻辑。根据我们的调查，本文是第一次研究的匹配逻辑的PIMP。在匹配逻辑中，我们将“无干扰”定义为字符并行规则，并证明了匹配逻辑对PIMP的操作语义的正确性。通过构造一个对配置模式执行符号化的逻辑语义重写的PIMP匹配逻辑验证器，将PIMP的操作语义和PIMP的验证形式化地联系起来，该验证器对PIMP的匹配逻辑是完善的。也就是说，我们的PIMP匹配逻辑验证器符合PIMP的操作语义。最后，通过一个并行程序设计中的标准问题，对匹配逻辑验证器进行了验证。
2021-02-08 cs.FL cs.LO
From Intuitionism to Many-Valued Logics through Kripke Models
直觉命题逻辑是由Kurt Gödel（1932）证明的无限多值逻辑，它是由Stanismartaw Jaumkowski（1936）证明的可数多值逻辑。在本文中，我们使用Saul Kripke（1959）的模型为这些定理提供了另一种证明。哥德尔的证明产生了一个中间命题逻辑（介于直觉主义和经典之间），现在被称为哥德尔或哥德尔-达米特逻辑，也被模糊逻辑学家研究。我们还提供了一些结果，在此逻辑命题连接词的可定义性。
2020-08-20 cs.LO math.LO
Undecidability and non-axiomatizability of modal many-valued logics
在这项工作中，我们研究了一类全球模态逻辑所产生的Kripke框架评估某些剩余格，在文献中称为模态多值逻辑的可判定性。我们展示了一个大的家庭，这些模态逻辑是不可判定的，与经典的模态逻辑和命题逻辑定义在同一类代数。这个家族包括了在标准Lukasiewicz代数和乘积代数上计算的Kripke框架所产生的全局模态逻辑。我们改进了前面的结果，证明了全局模态Lukasiewicz和乘积逻辑甚至不能递归可公理化。我们的结论是否定地解决了开放的问题，即每个全局模态逻辑是否与它的局部模态逻辑在无限制必然规则下是封闭的。
2022-04-15 cs.LO math.LO
Modular many-valued semantics for combined logics
本文利用部分非确定性矩阵上的通用运算，为组合逻辑构建可直接复用各成分逻辑多值语义的模块化语义，并分析有限值性、公理化、片段演算组合与可判定性保持条件。
2023-04-27 cs.LO math.LO
Foundations of Reasoning with Uncertainty via Real-valued Logics
IBM Research（IBM研究院）
实值逻辑是越来越多的神经符号方法的基础，尽管它们的逻辑推理能力通常只定性地描述。我们为建立这种系统的正确性和功能提供了基础。我们给出了一个健全的和强完备的公理化，可以参数化，以涵盖基本上每一个实值逻辑，包括所有常见的模糊逻辑。我们的句子类非常丰富，每个句子描述了实值逻辑的公式集合的一组可能的实值，包括哪些实值组合是可能的。强完备性允许我们精确地推导出关于给定的关于其他几个公式集合的实值组合的信息的公式集合的实值组合的信息。然后，我们扩展公理化处理加权子公式。最后，我们给出了一个基于线性规划的决策过程，对于某些实值逻辑，在某些自然假设下，我们的一组句子在逻辑上是否意味着另一个句子。
2022-08-30 cs.AI cs.LO
On the strongest three-valued paraconsistent logic contained in classical logic and its dual
LP $^{\supset,\mathsf{F}}$是一个三值次协调命题逻辑，本质上与J3相同。它的大多数属性都被认为是合理的次协调命题逻辑的理想属性。然而，从已经发表的结果可以很容易地得出，正好有8192个不同的三值次协调命题逻辑具有相关的性质。本文利用逻辑等价关系的性质来区分LP $^{\supset,\mathsf{F}}$与其它逻辑。作为专注于逻辑等价关系的奖金之一，它被发现，只有32的8192逻辑有一个逻辑等价关系，满足的单位，湮灭，幂等，和交换法律的合取和析取。LP $^{\supset,\mathsf{F}}$的大多数性质都被认为是合理的次协调命题逻辑的理想性质，而它的仿完全类似物也具有类似的性质。本文还利用逻辑等价关系的有关性质，将LP $^{\supset,\mathsf{F}}$的仿完全模拟与具有类似性质的其它三值仿完全命题逻辑区分开来。
2020-12-01 cs.LO math.LO
