首页 | 本学科首页   官方微博 | 高级检索  
     检索      


Deciding the existence of uniform interpolants over transitive models
Authors:Giovanna D??Agostino  Giacomo Lenzi
Institution:1. Dipartimento di Matematica e Informatica, Universit?? di Udine, Via delle Scienze 206, 33100, Udine, Italy
2. Dipartimento di Matematica e Informatica, Universit?? di Salerno, Via Ponte Don Melillo 1, 84084, Fisciano (SA), Italy
Abstract:We consider the problem of the existence of uniform interpolants in the modal logic K4. We first prove that all ${\square}$ -free formulas have uniform interpolants in this logic. In the general case, we shall prove that given a modal formula ${\phi}$ and a sublanguage L of the language of the formula, we can decide whether ${\phi}$ has a uniform interpolant with respect to L in K4. The ${\square}$ -free case is proved using a reduction to the G?del L?b Logic GL, while in the general case we prove that the question of whether a modal formula has uniform interpolants over transitive frames can be reduced to a decidable expressivity problem on the???-calculus.
Keywords:
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号