Finite sequent calculi for PLTL
Two sequent calculi for temporal logic of knowledge are presented: one containing invariant-like rule and the other containing looping axioms. Its proved that the calculi are equivalent, sound and complete.
Main Authors: | Romas Alonderis, Regimantas Pliuškevičius, Aida Pliuškevičienė |
---|---|
Format: | Article |
Language: | English |
Published: |
Vilnius University Press
2015-12-01
|
Series: | Lietuvos Matematikos Rinkinys |
Subjects: | |
Online Access: | https://www.journals.vu.lt/LMR/article/view/14916 |
Similar Items
-
Cut, invariant rule, and loop-check free sequent calculus for PLTL
by: Romas Alonderis, et al.
Published: (2011-12-01) -
Specialization of antecedent negation loop-rule for a fragment of propositional intuitionistic logic sequent calculus
by: Romas Alonderis
Published: (2009-12-01) -
A labeled sequent calculus for propositional linear time logic
by: Romas Alonderis
Published: (2012-12-01) -
A sequent calculus for propositional temporal logic with time gaps
by: Romas Alonderis
Published: (2011-12-01) -
Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus
by: Romas Alonderis
Published: (2008-12-01)