Partial cut elimination for propositional discrete linear time temporal logic | Zendy

Jūratė Sakalauskaitė | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Partial cut elimination for propositional discrete linear time temporal logic

Author(s) -

Jūratė Sakalauskaitė

Publication year - 2010

Publication title -

lietuvos matematikos rinkinys

Language(s) - English

Resource type - Journals

eISSN - 2335-898X

pISSN - 0132-2818

DOI - 10.15388/lmr.2010.63

Subject(s) - sequent , soundness , completeness (order theory) , natural deduction , sequent calculus , mathematics , linear temporal logic , cut elimination theorem , temporal logic , sketch , linear logic , propositional calculus , calculus (dental) , zeroth order logic , discrete mathematics , intuitionistic logic , proof calculus , algorithm , computer science , programming language , multimodal logic , mathematical analysis , description logic , medicine , geometry , dentistry , mathematical proof

We consider propositional discrete linear time temporal logic with future and past operators of time. For each formula ϕ of this logic, we present Gentzen-type sequent calculus Gr(ϕ) with a restricted cut rule. We sketch a proof of the soundness and the completeness of the sequent calculi presented. The completeness is proved via construction of a canonical model.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research