Tense logics based on posets
本文在基于偏序集的逻辑框架下研究真值随时间变化的动态逻辑,引入带偏好关系的时间集和时态算子,提出多种处理方法以推动后续研究。
2024-06-28 math.LO
Degree of Kripke-incompleteness of Tense Logics
本文将模态逻辑中Blok的Kripke不完备程度二分定理推广到时态逻辑格K、LT和NExt(ST),并证明这些格中迭代分裂恰好对应严格Kripke完备逻辑。
2025-09-24 math.LO
On Heyting algebras with negative tense operators
本文研究了赋有紧张负算子的Heyting代数,我们称之为紧张H-代数,并证明了这些代数是带Galois否定的直觉命题逻辑的代数语义。最后,我们将发展H-代数的Priestley型对偶。
2022-12-23 math.LO
Non-distributive logics: from semantics to meaning
我们讨论了一个正在进行的研究线的关系(非拓扑)语义的非分配逻辑。我们考虑的发展在技术上植根于对偶表征结果和统一对应理论的见解。然而,他们也有更广泛的,非分配逻辑,我们探讨的直观意义的概念分支。
2021-07-04 math.LO
Selfextensional logics with a distributive nearlattice term
我们定义了代数语言$\mathcal{L}$的三进制项$m$何时被称为代数逻辑$\mathcal{S}$的\textit{distributive nearlattice term}(DN项)。分配近格是Tarski代数和分配格的推广。通过对自扩张逻辑的代数对应体的代数中的DN-项的解释,我们证明了具有DN-项的自扩张逻辑。我们证明了与一个具有DN-项的自扩张逻辑相关联的代数的典范类(从抽象代数逻辑的观点来看)是一个簇,并且我们得到了这个逻辑实际上是完全自扩张的.
2018-02-11 math.LO
On the Cut Elimination of Weak Intuitionistic Tense Logic
本文提出一种通过分裂收缩规则和切割规则来证明弱直觉时态逻辑切割消去的新方法,并展望其未来理论扩展与应用。
2024-05-27 cs.LO math.LO
Pretabular Tense Logics over S4t
The Tsinghua-UvA JRC for Logic, Department of Philosophy, Tsinghua University(清华大学哲学系清华-阿姆斯特丹逻辑联合研究中心);Institute for Logic, Language and Computation, University of Amsterdam(阿姆斯特丹大学逻辑语言与计算研究所)
本文研究了S4t扩展的预表格时逻辑,定义了具有受限宽度、深度和z度的时逻辑S4BP,并证明了预表格逻辑在S4t扩展中的基数反二元定理。
2025-09-27 math.LO
Galois connections and tense operators on q-effect algebras
对于效应代数,所谓的时态算子已经由Chajda和Paseka引入。他们还提出了一个规范的建设,他们使用的概念,时间框架。时态算子表示量词“it is always going to the case that”和“it has always been the case that”,从而使我们能够在量子力学逻辑和多值逻辑中表示时间维度。关于时态算子的一个关键问题是它们的表示。有了一个带有时态算子的效应代数,我们可以问是否存在一个时间框架,使得这些算子中的每一个都可以通过规范构造得到。为了尽可能好地逼近物理实系统,我们引入了q-效应代数的概念,并解决了q-可表示的q-Jauch-Piron q-效应代数上的q-紧张算子的问题。
2018-09-11 math.LO
Toward the van Benthem Characterization Theorem for Non-Distributive Modal Logic
本文将模拟、互模拟及图像有限模型、模态饱和模型、超滤扩张和超幂扩张等模型论概念推广到非分配模态逻辑的极性语义,并据此证明了Hennessy-Milner定理与van Benthem刻画定理。
2024-04-08 math.LO
A Characterization Result for Non-Distributive Logics
本文将非分配逻辑归约为多类剩余模态逻辑,通过复用现有结果,成功将模态逻辑的 van Benthem 刻定结果推广至非分配逻辑。
2021-10-14 math.LO
Display to Labeled Proofs and Back Again for Tense Logics
我们介绍之间的翻译显示演算证明和标记演算证明的紧张逻辑的背景下。首先,我们证明了,在显示演算的最小时态逻辑Kt扩展与一般路径公理的每一个派生可以有效地转化为相应的标记演算的派生。关于逆翻译,我们表明,Kt扩展与路径公理,在相应的标记演算的每个派生可以放入一个特殊的形式,是可翻译的派生在相关的显示演算。在这个逆翻译中的一个关键见解是将显示序列规范表示为标记的多树。标记的多树,它表示等价类的显示序列模显示公设,也揭示了相关的对应结果紧张的逻辑。
2021-05-06 cs.LO math.LO
Priestley-style duality for filter-distributive congruential logics
本文为带定理的同余、有限且滤子分配逻辑的代数类提出 Priestley 风格对偶,并分析对偶空间性质与逻辑性质(如演绎定理、析取存在性)的对应关系。
2025-10-11 math.LO
Strong Completeness and the Finite Model Property for Bi-Intuitionistic Stable Tense Logics
双直觉稳定时态逻辑(英语:Bi-Intuitionistic Stable Tense Logics)是一种具有克里普克语义的时态逻辑,其中框架中的世界配备有前序以及相对于该前序“稳定”的可达性关系。BIST逻辑是在超图的语义背景下产生的逻辑BiSKt的扩展,因为预序的特殊情况可以表示超图的关联结构。在本文中,我们提供了,第一次,一个希尔伯特式公理化的BISKt和证明强完备性的BiSKt。我们继续证明强完备性的一类BIST逻辑得到的BiSKt由一定形式的公式扩展。此外,我们还证明了一类BIST逻辑的有限模型性质和可判定性。
2017-03-07 cs.LO math.LO
Most Properties are Undecidable for Transitive Tense Logics
The Tsinghua-UvA JRC for Logic Department of Philosophy Tsinghua University(清华大学哲学系清华-阿姆斯特丹逻辑联合研究中心);Institute for Logic, Language and Computation University of Amsterdam(阿姆斯特丹大学逻辑、语言与计算研究所)
本文通过从Minsky机器的不可判定问题归约,证明了传递时态逻辑格NExt(K4t)中大多数性质(如Kripke完全性、有限模型性质和可判定性)是不可判定的。
2026-09-11 cs.LO math.LO
The proof theory and semantics of second-order (intuitionistic) tense logic
本文提出二阶直觉时逻辑的公理化、证明论和模型论定义,并证明其一致性,同时通过证明搜索论证建立了标签序列演算的完备性。
2026-02-05 cs.LO math.LO
Distributive abstract logics and the Esakia duality
在本文中,我们开发了一个几乎通用的过程,从布朗和Suszko意义上的抽象逻辑格。用这种方法可以建立抽象逻辑的某些范畴与相应的拓扑空间范畴之间的对偶。更详细地,我们将解释具有直觉态射的抽象直觉主义逻辑范畴和具有Esakia态射的Esakia空间范畴之间的对偶性。
2014-10-29 math.LO
Representations of bounded distributive lattices as the continuous sections of Sheaves based on the Priestly and Zarski topologies
利用Comer关于柱形代数的层对偶理论,给出了分配有界格按模态(分布在联上的函数)扩张为层的连续截面的一个表示定理.我们的表示是通过一个反变函子定义的。我们给应用程序的多值逻辑逻辑和各种修改的一阶逻辑和多模态逻辑,设置在一个代数框架。
2013-04-02 math.LO
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
本研究提出一种基于无切割嵌套序列演算的纯句法方法,证明含逆模态的经典时态逻辑及其扩展、双直觉主义逻辑的Craig插值性质,创新引入定义插值元对偶的正交性条件,无需语义或嵌入辅助。
2023-06-14 cs.LO math.LO
Definite Descriptions and Hybrid Tense Logic
本文构建了以谓词抽象和限定摹状词为唯一非严格词项的一阶混合时态逻辑,用处理 sat-公式的表推演演算形式化,并构造性证明插值定理,扩展了 Blackburn 与 Marx 的结果。
2024-12-02 cs.LO math.LO
Compatibility between modal operators in distributive modal logic
本文识别了分配模态逻辑中保证 box 和 diamond 算子源自同一可达关系且不施加额外限制的基本相容性条件,并通过添加局部性公理模块化地获得直觉主义和正模态逻辑。
2023-11-16 math.LO
Realizing the Maximal Analytic Display Fragment of Labeled Sequent Calculi for Tense Logics
本文通过提出PTIME翻译和严格标签证明概念,建立了时态逻辑解析展示演算与标签相继式演算之间的多项式等价关系,证明标签形式体系包含并扩展了展示形式体系。
2024-06-28 cs.LO math.LO
Non-distributive relatives of ETL and NFL
本文构造了ETL和NFL的非分配相对逻辑,使用非分配格M3作为真值格,提供解析表列系统并证明其正确性与完备性。
2024-03-14 math.LO
Set Representation of Dynamic De Morgan algebras
一个德摩根代数是指一个有界偏序集配备了一个反调对合视为否定。这样的代数可以被认为是满足双重否定律的命题逻辑的代数公理化。我们的目的是在每一个De Morgan代数中引入所谓的时态算子,以得到一个具有满足双重否定律的否定的时态逻辑的代数对应,而不必是布尔的。在时态算子$G$和$H$用框架构造的基础上,我们解决了如下问题:如果给定一个动态De Morgan代数,如何找到一个框架,使得它的时态算子$G$和$H$可以用这个框架构造.
2018-10-11 math.LO
An algebraic analysis of implication in non-distributive logics
在本文中,我们引入了(格)斜希尔伯特代数的概念作为希尔伯特代数的自然推广。这个概念允许统一处理几个结构的突出重要性的数理逻辑,例如(广义)正交模格,和MV-代数,其中承认一个自然的概念的影响。事实上,斜希尔伯特代数对(强)分段伪补偏序集的作用与希尔伯特代数对相对伪补偏序集的作用相似。我们将讨论斜希尔伯特代数的闭元、稠密元和弱稠密元的基本性质及其应用,并给出它们的结构理论的一些基本结果。
2021-05-18 math.LO
Non-distributive description logic
本研究提出基于非分配格命题逻辑的描述逻辑LE-ALC,在FCA形式背景的关系结构上解释语义,给出检验带无环TBox知识库一致性的tableaux算法并证明其性质,且该场景下一致性检验复杂度低于经典ALC。
2024-04-14 math.LO
Bounded distributive lattices with strict implication and weak difference
本文引入 WHB-代数,建立其关系型类 Priestley 对偶性,并借助时态扩张证明该簇的有限模型、合并、同余扩张及 Maehara 插值等性质。
2023-12-18 math.CT math.LO
Monotonic Distributive Semilattices
在与非经典逻辑相关的代数研究中,(分配)半格总是处于背景中。例如,直觉主义逻辑的$\{\rightarrow,\wedge,\top\}$ -片段的代数语义是蕴涵交半格\cite{CelaniImplicative} \cite{ChajdaHalasKuhr}的变体。本文引入并研究了赋单调模态算子的分配交半格类$m$。我们利用标准扩张理论研究了这些代数的表示论,并给出了它们的拓扑对偶。此外,我们展示了我们的新的对偶扩展到一些特定的子类。
2018-10-19 math.LO
On the structure of modal and tense operators on a boolean algebra
本文研究布尔代数上必然、可能及时态算子的偏序集结构,证明其并半格性质及完备条件下的frame性质,并利用Jonsson-Tarski对偶性刻画对应关系。
2025-04-23 math.GN math.LO
Space and time via Topological and Tense cylindric algebras
设$α$为任意序数,$2<n<ω$。在被《数学学报》接受出版的\cite{3}中,我们简要地研究了用$α$多变量进行拓扑逻辑的代数逻辑、插值、合并和$α$多变量$\sf TopL_α$。这是一个续集\cite{3} ;第二部分模态柱形代数,在那里我们研究代数其他属性的$\sf TopL_α$。模态柱形代数是无限维的柱形代数,用一元模态扩展,从单峰逻辑$\sf L$(如$\sf K5$或$\sf S4$)继承其语义。使用代数逻辑的方法,我们研究符号$\sf TCA_α$中的拓扑(当$\sf L=S4$时)。研究了$\sf TopL_ω$和$\sf TenL_ω$的完备性和省略型$\sf OTT$ s,证明了局部有限的这类代数的几个表示性结果.此外,我们研究了原子规范性的概念,为${\sf TCA}_{n}$和${\sf TenL}_n$,一个众所周知的持久性属性模态逻辑,在$\sf OTT$的${\sf TopL}_n$和${\sf TeLCA}_n$,分别。研究了拓扑柱形代数的可表示性、省略类型、插值和复杂性问题(如不可判定性).在本文的续集中,我们介绍了时间cylindric代数,并指出如何合并代数的空间(拓扑代数)和代数的时间(时间代数)形成拓扑-时间柱形代数,使自己包含时空gemetries,在一个纯粹的代数方式。
2020-05-18 math.LO
Algorithmic correspondence and canonicity for non-distributive logics
我们扩展理论的统一对应到一个非常广泛的类的逻辑与代数语义给出了各种正常的格展开(LE),也被称为“格与运营商”。具体来说,我们引入了一个非常一般的语法定义类的Sahlqvist公式和不等式,它适用于统一的每个LE-签名,并给出纯粹的顺序理论的性质的代数解释的逻辑连接词。与此同时,我们介绍了一个变种的算法ALBA,具体的设置LE,有效地计算一阶对应的LE-不等式,并保证成功的广泛的一类不等式(所谓的归纳不等式)显着扩展Sahlqvist类。此外,我们表明,ALBA成功的每一个不等式是典型的。这些结果的投影产生了许多著名的子结构逻辑的最先进的对应理论,例如Lambek演算及其扩展,Lambek-Grishin演算,德摩根格的逻辑(不一定是分配的),以及线性逻辑的乘法-加法片段。
2016-04-04 math.LO
The logic of effect algebras incorporating time dimension
引入效应代数是为了描述效应的结构,即量子力学中的事件。它们是描述相应事件背后逻辑的部分代数。如何在有效代数中引入逻辑联系蕴涵是很自然的问题。对于格序效应代数,这个任务已经由几位作者解决了,包括本书的作者。我们专注于效应代数,不需要格序,因为这些可以更好地描述发生在量子物理系统中的事件。虽然一个效果代数只是部分的,我们试图找到一个逻辑连接蕴涵是处处定义的。但是这样的连接词可以是“不清晰的”或“不精确的”,因为它对于给定的条目对的输出不需要是基础效应代数的元素,而是可以是(相互不可比的)极大元的子集。我们引入了这样一个蕴涵及其表示合取的伴随函子。然后我们考虑效应代数上的所谓紧张算子。当然,这些运算符在上述意义上也是“不尖锐”的,但它们与运算符的蕴涵和合取有一定的关系。最后,对于给定的时态算子和给定的时间集T,我们描述了两种方法如何构造T上的时间偏好关系R,使得给定的时态算子与时间框架(T,R)所诱导的时态算子相比较或等价。
2023-03-20 math.LO
A non-distributive logic for semiconcepts of a context and its modal extension with semantics based on Kripke contexts
分别对纯双布尔代数和带算子的纯双布尔代数类提出了一个非分配的两类超代数演算\textbf{PDBL}及其模态扩张\textbf{MPDBL}.接下来提出了\textbf{PDBL}的关系语义,其中任何公式都被解释为上下文的概念。对于\textbf{MPDBL},关系语义基于Kripke上下文,并且公式被解释为底层上下文的概念。该系统被证明是健全和完整的关系语义。将适当的序列添加到\textbf{MPDBL}导致具有基于自反、对称或传递Kripke上下文的语义的逻辑。这些系统之一是拓扑纯双布尔代数的逻辑。证明了利用\textbf{PDBL}可以表达概念知识的基本概念和关系,并可以得到涉及否定的推理。此外,绘制与粗糙集合论,上下近似的概念的上下文定义的连接。然后,它表明,使用公式和序列涉及模态算子在\textbf{MPDBL},这些近似算子和它们的属性可以被捕获。
2022-07-22 math.LO
Superamalgamation for modal lattices via non-distributive dualities
Institute for Logic, Language and Computation, Universiteit van Amsterdam(逻辑、语言与计算研究所,阿姆斯特丹大学);Department of Mathematics, Université du Luxembourg(数学系,卢森堡大学)
本文通过非分配对偶性证明模态格的超拼接性质,并由此得出弱正模态逻辑具有Craig插值性质,同时扩展到其他弱正模态逻辑。
2026-03-16 math.LO
Non-distributive positive logic as a fragment of first-order logic over semilattices
我们把非分配正逻辑看作是一个单排序的一阶语言的片段,它被一个新的模拟概念所保存,称为满足模拟。相遇模拟与模拟的区别在于它们将一个模型的状态对与另一个模型的单个状态联系起来。在这个结果的途中,我们使用一个更传统的模拟概念,并证明了它的Hennessy-Milner风格的定理,使用类似的模态饱和称为满足紧凑性。
2023-02-06 cs.LO math.LO
The logic of quantum mechanics incorporating time dimension
与经典的命题演算在代数上基于布尔代数类似,量子力学的逻辑也是基于G. Birkhoff和J. von Neumann和K.胡西米然而,这个逻辑并不包含时间维度,尽管很明显,量子力学逻辑中出现的命题依赖于时间。本文的目的是表明,所谓的时态算子也可以引入这样的逻辑给定的时间集和给定的时间偏好关系。在这种情况下,我们可以用纯代数的方法引入这些算子。我们得出这样的运营商的几个重要性质,特别是我们表明,他们形成动态对,并在一起,一个动态代数。我们调查这些运营商的连接与逻辑连接词,连接和蕴涵来自佐佐木投影。然后,我们解决了逆问题,即找到给定的时间集和给定的紧张运营商的时间偏好关系,以便产生的时间框架诱导给定的运营商。我们表明,给定的运营商可以得到一个适当的扩展的时间框架引起的运营商的限制。
2022-11-15 math.LO
Topological representation of intuitionistic and distributive abstract logics
我们继续我们早期论文的工作(Lewitzka和Brunner:Minimally generated abstract logics,Logica Universalis 3(2),2009),其中研究了抽象逻辑,特别是直觉抽象逻辑。抽象逻辑可以直接自然地拓扑化。这有利于拓扑研究类的具体逻辑时,他们给出了抽象的形式。此外,这种直接的拓扑方法避免了通常用于表示逻辑的复杂的代数和格论机器。基于这一观点,本文定义了以稳定逻辑映射为态射的直觉抽象逻辑范畴和以谱映射为态射的蕴涵谱空间范畴。我们证明了这些范畴的等价性,并得出结论,分配抽象逻辑和分配清醒空间的更大的范畴是等价的。
2015-08-18 cs.LO math.LO
On Tense MV-algebras
本文的主要目的是研究时态MV-代数,即具有新的一元运算$G$和$H$的MV-代数,它们表示一个泛时间量词.紧MV-代数是D. Diagonescu和G.乔治斯库利用MV-代数之间的一个新的fm-函数的概念,我们\zruseno{will prove}了任何时态半单MV-代数都是由一个时间框架诱导的,类似于这一逻辑领域的经典著作。作为副产品,我们得到了MV-代数上的极值状态的一个新的特征。
2013-05-15 math.AC math.LO
Sahlqvist theory for impossible worlds
我们将统一对应论推广到不可能世界的Kripke框架及其相关的正则模态逻辑。这些逻辑的模态联结不需要是正规的:只需要较弱的可加性和乘法性。在概念上,有人认为,它们缺乏必要性,使得规则模态逻辑比正常的模态逻辑更适合在形式化的认识和道义设置。从技术的角度来看,正则性被证明是非常自然的,足以处理代数正规性约翰逊式。事实上,加法性和乘法性是将琼森最初的规范性证明扩展到某些正则分配模态逻辑的完整萨尔奎斯特类的关键,自然地概括了分配模态逻辑。最有趣的是,加性和乘性也是原始(即正常)DML中约翰逊式正规性的关键。我们的贡献包括:在分配格命题基上定义了正则模态逻辑的Sahlqvist不等式,证明了它们遵循Jónsson策略的规范性,并将ALBA算法应用于两个非经典的正则模态逻辑的构造(分配格和直觉)的基础,证明适应ALBA是保证成功的语法定义的类,其中适当地包括Sahlqvist一个;最后,应用前面的结果,代替Kripke的证明,证明了Lemmon的认知逻辑E2-E5关于具有不可能世界的Kripke框架的初等类的强完备性。
2016-03-27 math.LO
Many-valued aspects of tense an related operators
基于Halmos工作与时态算子研究,构建三个基本构造,生成四个协变和两个逆变函子,建立三个伴随情境,应用于代数、逻辑和拓扑。
2025-04-24 math.CT math.LO
Another look on tense and related operators
出于经典的工作哈尔莫斯功能一元布尔代数,我们得出三个基本的超半格建设,除其他事项外,所谓的幂集和幂集运营商。这样的构造非常有用,几乎可以在现代数学的所有分支中找到,包括代数,逻辑和拓扑。我们的三个结构产生四个协变和两个反变函子,并构成三个伴随的情况下,我们在简单的例子说明。
2022-07-12 math.LO math.RA
A categorical equivalence for monadic algebras of first-order substructural logics motivated by Kalman's construction
School of Science, Xi’an Shiyou University(西安石油大学理学院);School of Science, Xi Hang University(西安航天大学理学院);CONICET and Departamento de Matematica, Facultad de Ciencias Exactas, Universidad Nacional del Centro de la Provincia de Buenos Aires(阿根廷布宜诺斯艾利斯省中部国立大学精确科学学院数学系与阿根廷国家科学研究委员会)
本文通过卡曼构造,研究单子余分配格的范畴等价性,并扩展了相关领域的研究成果。
2026-01-29 math.LO
Frobenius Galois expansions of substructural logics:Algebraization, Kalman equivalence and positive cone semantics
School of Science, Xi’an Petroleum University(西安石油大学理学院);School of Mathematics and Data Science, Shaanxi University of Science and Technology(陕西科技大学数学与数据科学学院);School of Science, Xi Hang University(西航大学理学院)
本文引入子结构逻辑FL_ew的Frobenius-Galois扩张,证明其可代数化,建立Kalman等价与正锥语义,统一了代数、范畴与逻辑框架。
2026-09-10 math.LO
The Distributive Full Lambek Calculus with Modal Operators
本文研究了在非交换条件下,考虑$\Box$和$\Diamond$的带有模态算子的有界分配剩余格的逻辑。我们为这样的子结构模态逻辑引入关系语义。通过离散对偶和正则扩张证明了任何正则逻辑都是Kripke完备的。也就是说,我们表明,一个模态扩展的分配充分Lambek演算是其框架的逻辑,如果它的品种是封闭的规范下的扩展。在此基础上,我们建立了剩余分配模态代数与基于Priestley空间的拓扑Kripke结构之间的Priestley式对偶。
2020-05-31 math.CT math.LO math.RA
Finite axiomatizability of logics of distributive lattices with negation
本文主要研究由各种带否定的分配格定义的保序逻辑,特别是研究这些逻辑是否可以通过有限希尔伯特演算公理化的问题。在否定结果的一面,我们提供了一个句法条件上的等式表示的品种,需要失败的有限公理化相应的逻辑。这个结果的一个应用是所有带否定的分配格的逻辑不是可公理化的;同样,我们建立了所有奥卡姆代数的簇的保序逻辑也不是可公理化的。在积极的一面,我们表明,半德摩根代数的任意子品种是公理化的有限数量的方程,当且仅当相应的保序逻辑公理化的有限希尔伯特演算。这个等价也适用于奥卡姆代数的伯曼簇的每个子簇。作为推论,我们得到了直觉主义逻辑的无蕴涵部分是可公理化的新证明,以及一个新的希尔伯特演算.我们的证明是建设性的,因为它们允许我们有效地将各种代数的等式表示转换为相应的保序逻辑的希尔伯特演算,反之亦然.我们还考虑了与上述变种相关的断言逻辑,特别表明半德摩根代数的可公理化的子变种的断言逻辑也是可公理化的。
2021-02-10 cs.LO math.LO
Unified Correspondence and Proof Theory for Strict Implication
分配格扩展逻辑(DLE-逻辑)的统一对应理论是严格蕴涵逻辑的专门理论。作为一般语义守恒性结果的结果,广泛的严格蕴涵逻辑可以保守地扩展到有界分配全非结合Lambek演算(BDFNL)上的Lambek演算。许多严格的蕴涵序列可以转化为分析规则,采用统一对应理论的主要工具之一,即(适当修改的版本)基于阿克曼引理的算法$\msf{ALBA}$。给出了BDFNL的Gentzen型无割演算及其推广,并给出了由严格蕴涵序列转化而来的解析规则。
2016-04-29 math.LO
Recovery operators in quasi-Nelson logic: the prelinear case
IIIA-CSIC(西班牙科学理事会人工智能研究所);UNED(西班牙国立远程教育大学)
研究准Nelson逻辑中的一致性和确定性算子,在预线性条件下推广了LFIs/LFUs的结果,无需对合性假设。
2026-07-01 math.LO
Algebraic analysis of temporal and topological finite variable fragments, using cylindric modal algebras
我们研究我们称之为拓扑柱形代数和紧张柱形代数定义的每一个序数$α$。前者是以$α$为索引的$\sf S4$模态展开的维数为$α$的柱形代数。可表示拓扑代数的语义是由定义在其基上的拓扑的内部运算导出的。时态柱形代数是由模态$F$(未来)和$P$(过去)代数谓词时态逻辑扩展的柱形代数。我们证明了有限维$n>2$的紧张和拓扑柱形代数的无限多个变种包含和包括各种各样的维数$n$的可表示代数不是原子标准的。我们表明,任何类包含类的完全表示代数有一个弱整洁嵌入性质是不是小学。从这两个结果中,我们得出了谓词拓扑和时态逻辑的有限变量片段的省略类型相同的结论。我们表明,通常版本的省略类型定理限制到这样的片段时,变量的数量是$>2$显着失败,即使我们大大拓宽了类模型允许省略一个单一的非主要类型的可数原子理论,即非主要类型consting的co原子。
2014-02-02 math.LO
Join-semilattices whose principal filters are pseudocomplemented lattices
本文讨论了其部分(即主滤子)是伪补格的并半格。[b,1]节中\vee b的伪补记为\rightarrow b,它可以看作是某种直觉主义逻辑中的连接蕴涵.与Brouwerian半格的情况相反,截面不必是分配格。这基本上允许在非经典逻辑中的可能应用。我们提出了一个连接的半格中提到的所谓的非经典蕴涵半格,可以转换成I-代数具有处处定义的操作。此外,我们把我们的结构与分段的和相对剩余的半格联系起来,这意味着我们的逻辑结构与子结构逻辑密切相关。证明了I-代数构成一个同余分配的、3-置换的弱正则簇。
2021-05-15 math.LO
Labelled calculi for the logics of rough concepts
本文针对非分配正规模态逻辑 L 及其扩张,利用丰富化形式背景的一阶原子公式作标签,构建可靠完备的加标矢列演算,并扩展得到粗糙形式背景逻辑的证明系统。
2024-01-18 math.LO
A Framework for Intuitionistic Grammar Logics
我们将直觉时态逻辑推广到多模态的情况下,把语法逻辑的直觉的基础。我们提供公理化一类基地直觉语法逻辑,以及提供公理化的扩展与组合的序列性公理和我们所说的“直觉路径公理”。我们表明,每个公理化是健全的,完整的完整性,通过一个典型的规范模型的建设。
2021-10-02 cs.LO math.LO
Topological Duality for Distributive Lattices: Theory and Applications
本书系统讲解Stone-Priestley对偶性理论,旨在快速提供全面的对偶工具,并将其应用于命题逻辑语义、逻辑形式的域理论及profinite monoids理论等三大标志性领域。
2023-04-05 cs.LO math.LO
The Topological and Logical Structure of Concurrency and Dependency via Distributive Lattices
本文的动机是希望研究包管理使用的工具包的语义的函数式语言。正如它所揭示的那样,这与并发计算的语义密切相关。我们制作的模型不仅具有理论意义,而且可以进行分析和计算。这项工作作出了一些相关的贡献。首先,它涉及分支依赖结构的规范,存在于从知识表示到包管理的领域,并发计算的语义规范。其次,它以精确的方式将依赖结构与格相关联,与特定的格子类建立完全对应。然后,它利用这一点作为一个关键的成分,再加上未得到充分重视的Bruns-Lakser完成,在相关的依赖结构,以区域设置-对象配备了拓扑和逻辑属性。然后,它提供了一个例子,说明这种属性的相互作用是如何使用的-使用依赖结构的拓扑属性来为相关区域设置的内部逻辑配备表示收缩关系(即“版本控制”)的模态。这种方法让我们看到链接(或者更确切地说,选择链接的对象,即“解决”)作为一种效果。最后,它讨论了这种结构可能涉及到复杂性理论中的重要问题,包括可满足性问题的解决方案。在此过程中,我们将看到这种方法如何与熟悉的对象相关,例如包版本策略,Merkle树,nix操作系统和分布式版本控制工具,如git。
2020-04-12 cs.LO math.LO
Labelled calculi for lattice-based modal logics
本文为基本正规非分配模态逻辑L及其31个公理化扩张提出了带标签矢列演算,并证明了其可靠性、完备性、保守性、切割消去与子公式性质,展示了为LE-逻辑类系统引入带标签演算的统一方法。
2024-01-18 math.LO
Game semantics for lattice-based modal μ-calculus
本研究将模态μ-演算拓展为基于格的非分配版本并用于分类场景形式化,构建了对应的博弈语义并证明其恰当性,还定义了极性互模拟并验证了该演算在其下的不变性。
2024-08-13 math.LO