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 darbas apsaugotas Creative Commons priskyrimo 4.0 viešąja licencija.