Open AccessA sequent calculus for propositional temporal logic with time gaps
Author(s) -
Romas Alonderis
Publication year - 2011
Publication title -
lietuvos matematikos rinkinys
Language(s) - English
Resource type - Journals
eISSN - 2335-898X
pISSN - 0132-2818
DOI - 10.15388/lmr.2011.ml01
Subject(s) - sequent calculus , cut elimination theorem , sequent , proof calculus , natural deduction , calculus (dental) , propositional variable , zeroth order logic , mathematics , propositional calculus , well formed formula , curry–howard correspondence , kripke semantics , computer science , discrete mathematics , intermediate logic , programming language , multimodal logic , description logic , mathematical proof , medicine , geometry , dentistry
A sequent calculus with Kripke semantics internalization for a propositional temporal logic with time gaps is introduced. All rules of the calculus are context-free andheight-preserving invertible. Structural rules are admissible. The calculus is cut free and is proved to be complete.