Pasiūlyta dedukcija pagrįsta išprendžiamoji procedūra išplėstam minisferiniam pirmos eilės tiesinio laiko logikos (FT L) su lygybe fragmentui. Pasiūlyta išprendžiamoji procedura yra korektiška ir pilna.
Šis kūrinys yra platinamas pagal Kūrybinių bendrijų Priskyrimas 4.0 tarptautinę licenciją.