Pasiūlyta dedukcija pagrįsta išsprendžiamoji procedūra miniskopizuotam pirmos eilės kvantorinės skaidaus laiko logikos fragmentui. Pasiūlyta išsprendžiamoji procedūra yra korektiška ir pilna.
Šis kūrinys yra platinamas pagal Kūrybinių bendrijų Priskyrimas 4.0 tarptautinę licenciją.