探索直觉主义时态逻辑的丛林
摘要：直觉主义时间逻辑在计算机科学和人工智能领域的重要性在最近几年变得越来越明确。 从证明论的观点来看，通过类型理论，直觉主义时间逻辑使得可以向函数语言添加新功能，而从语义的角度来看，关于动态系统的推理和逻辑编程的几个逻辑及其语义都起源于这个框架。在本文中，我们考虑了几个直觉主义线性时态逻辑的公理系统，并证明这些系统中的每一个都适用于基于Kripke框架或动态拓扑系统的结构类。我们的拓扑语义具有对`此后'模态性的新解释，这是经典模态性的自然直觉主义变体。利用这些正确性结果，我们证明从公理系统中得到的七个逻辑是不同的。
作者：Joseph Boudou and Mart''in Di''eguez and David Fern''andez-Duque and Philip Kremer
论文ID：1912.12895
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22