Back to Search
Start Over
Įrodymo ciklų metodas laiko logikai
- Source :
- Lietuvos matematikos rinkinys. Ser. A, Vilnius : Vilniaus universiteto leidykla, 2019, t. 60, p. 1-6, Lietuvos Matematikos Rinkinys, Vol 60, Iss A (2019)
- Publication Year :
- 2019
-
Abstract
- Various types of calculi (Hilbert, Gentzen sequent, resolution calculi, tableaux) for propositional linear temporal logic (PLTL) have been considered in the literature. Cutfree Gentzen-type sequent calculi are convenient tools for backward proof-search search of formulas and sequents. In this paper we present a cut-free Gentzen type sequent calculus for PLTL with the operator “until”. We show that the calculus is sound and complete for the considered logic.
Details
- Language :
- Lithuanian
- ISSN :
- 01322818 and 2335898X
- Database :
- OpenAIRE
- Journal :
- Lietuvos matematikos rinkinys. Ser. A, Vilnius : Vilniaus universiteto leidykla, 2019, t. 60, p. 1-6, Lietuvos Matematikos Rinkinys, Vol 60, Iss A (2019)
- Accession number :
- edsair.doi.dedup.....10317c07c15346fc43bbbc834b0c6323