A decidable fragment of first order modal logic: two variable term modal logic
Padmanabha, Anantha and Ramanujam, R (2023) A decidable fragment of first order modal logic: two variable term modal logic. ACM Transactions on Computational Logic. pp. 137.
Text
 Accepted Version
Restricted to Repository staff only Download (1MB)  Request a copy 
Abstract
First order modal logic (FOML) is built by extending First Order Logic (FO) with modal operators. A typical formula is of the form ∀x∃y□P(x,y) . Not only is FOML undecidable, even simple fragments like that of restriction to unary predicate symbols, guarded fragment and two variable fragment, which are all decidable for FO become undecidable for FOML. In this paper we study Term Modal logic (TML) which allows modal operators to be indexed by terms. A typical formula is of the form ∀x∃y □xP(x,y) . There is a close correspondence between TML and FOML and we explore this relationship in detail in the paper. In contrast to FOML, we show that the two variable fragment (without constants, equality) of TML is decidable. Further, we prove that adding a single constant makes the two variable fragment of TML undecidable. On the other hand, when equality is added to the logic, it looses the finite model property.
Item Type:  Article  

Authors:  Padmanabha, Anantha and Ramanujam, R  
Document Language: 


Subjects:  Computer science, information & general works Azim Premji Foundation Structure > Azim Premji University > Computer science, information & general works 

Divisions:  Azim Premji University  
Full Text Status:  Restricted  
Related URLs:  
URI:  http://publications.azimpremjiuniversity.edu.in/id/eprint/4779  
Publisher URL: 
Actions (login required)
View Item 