Pasiūlyta dedukcija pagrįsta išsprendžiamoji procedūra miniskopizuotam pirmos eilės dinaminės 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ą.