文章基本信息

标题：A Decidable Intuitionistic Temporal Logic
本地全文：下载
作者：Joseph Boudou ; Mart{\'i}n Di{\'e}guez ; David Fern{\'a}ndez-Duque 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：82
页码：14:1-14:17
DOI：10.4230/LIPIcs.CSL.2017.14
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We introduce the logic ITL^e, an intuitionistic temporal logic based on structures (W,R,S), where R is used to interpret intuitionistic implication and S is an R-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for ITL^e are decidable. We prove this by showing that the logic enjoys the strong finite model property. In contrast, we also consider a 'persistent' version of the logic, ITL^p, whose models are similar to Cartesian products. We prove that, unlike ITL^e, ITL^p does not have the finite model property.
关键词：intuitionistic logic; temporal logic; products of modal logics