
Cut elimination for knowledge logic with interaction
Author(s) -
Julius Andrikonis,
Regimantas Pliuškevičius
Publication year - 2021
Publication title -
lietuvos matematikos rinkinys
Language(s) - English
Resource type - Journals
eISSN - 2335-898X
pISSN - 0132-2818
DOI - 10.15388/lmr.2007.24226
Subject(s) - axiom , construct (python library) , type (biology) , mathematics , sequent calculus , discrete mathematics , computer science , calculus (dental) , algebra over a field , pure mathematics , programming language , medicine , ecology , geometry , dentistry , mathematical proof , biology
In the article the multimodal logic Tn with central agent interaction axiom is analysed. The Hilbert type calculi is presented, then Gentzen type calculi with cut is derived and the proof of cutelimination theorem is outlined. The work shows that it is possible to construct a Gentzen type calculi without cut for this logic.