Įrodymo paieškos automatizacija pirmos eilės, tiesinio laiko logikos fragmentui - Alonderis, Romas (Lietuvos matematikos rinkinys, 2003)
Naudojant Pascalio programavimo kalbą buvo parašyta programa, realizuojanti krodymo paieškos procedūrą, skirtą vienam pirmos eilės tiesinio laiko logikos išsprendžiamam fragmentui. Darbe yra aptariami kai kurie šios programos veikimo principai, įvertinamas jos sudėtingumas.