Cut, invariant rule, and loop-check free sequent calculus for PLTL
Copyright policy )Cut, invariant rule, and loop-check free sequent calculus for PLTL
In this paper, some loop-check free saturation-like decision procedure is proposed for propositional linear temporal logic (PLTL) with temporal operators “next” and “always”. This saturation procedure terminates when special type sequents are obtained. Properties of PLTL allows us to construct backtracking-free decision procedure without histories and loop-check.
- Vilnius University Lithuania
Decision procedure, termination, temporal logics, loop-check, decision procedure, Sequent calculus, Išsprendimo procedūra, Temporal logics, sequent calculus, Loop-check, QA1-939, Ciklų tikrinimas, Mathematics, Termination, Sekvencinis skaičiavimas, Laiko logika
Decision procedure, termination, temporal logics, loop-check, decision procedure, Sequent calculus, Išsprendimo procedūra, Temporal logics, sequent calculus, Loop-check, QA1-939, Ciklų tikrinimas, Mathematics, Termination, Sekvencinis skaičiavimas, Laiko logika
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).0 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!