Search

Showing total 2 results
2 results

1. Įrodymo ciklų metodas laiko logikai

Author

Haroldas Giedra and Romas Alonderis

Subjects
sequent calculi, LOOP (programming language), temporal logics, lcsh:Mathematics, Sequent calculus, Resolution (logic), Type (model theory), derivation loops, lcsh:QA1-939, Operator (computer programming), Linear temporal logic, Calculus, Temporal logic, Sequent, Mathematics
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.

Published
2019

2. Dubliavimo eliminavimas modalumo logikoms S5 ir KD45

Author

Regimantas Pliuškevičius and Julius Andrikonis

Subjects
termination, contraction-free, Backtracking, lcsh:Mathematics, Modal logic, Sequent calculus, Natural number, lcsh:QA1-939, backtracking, sequent calculus, Modal, Contraction-free, Termination, Calculus, Sequent, Contraction (operator theory), Axiom, modal logic, Mathematics
Abstract

It is known that termination and backtracking are among the most important problems in constructing derivations in non-classical logics. In this paper contractionfree and backtracking-free sequent calculi for modal logics S5 and KD45 are presented and founded. These are index-style sequent calculi with some specific indexed axioms. The main new ideas in considered calculi are to use metavariables (along with natural numbers) as elements of indexes and to numerate by different natural number all the positive occurrences of modality 2.

Published
2011