Restrictions for loop-check in sequent calculus for temporal logic with until operator
Copyright policy )Restrictions for loop-check in sequent calculus for temporal logic with until operator
In this paper, we present sequent calculus for branching-time temporal logic with until operator. This sequent calculus uses efficient loop-checktechinque. We prove that we can use not all but only several special sequents from the derivation tree for the loop-check. We use indexes to discover these special sequents in the sequent calculus. These restrictions let us to get efficient decision procedure based on introduced sequent calculus.
- Vilnius University Lithuania
sequent calculus, until operator, ciklų radimas, loop-check, until operatorius, QA1-939, sekvencinis skaičiavimas, branchnig-time temporal logic, skaidaus laiko logika, Mathematics
sequent calculus, until operator, ciklų radimas, loop-check, until operatorius, QA1-939, sekvencinis skaičiavimas, branchnig-time temporal logic, skaidaus laiko logika, Mathematics
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!