Strateegiad.

Sekventsarvutus on heaks aluseks tõestuse otsingu strateegiatele, kuid automaatsel kujul ei ole see väga praktiline. Tüüpilisel juhul on sekventsis palju valikuid, millist reeglit kasutada, ja nii igal tõestuse sammul. Kui meil pole võimalust vähemalt osa sellest paljususest välja rookida, siis upume peagi valikute hulka.
Vaatleme alustuseks kaht meetodit, mis vähendavad otsingu mitte-determineeritust.
- Esimene neist vaatleb pööramisomadusi, mis kehtivad siis, kui järeldusreegli eeldused on tuletatavad siis ja ainult siis, kui järeldus on tuletatav.
- Teine uurib fokuseerimisomadusi, mis lubavad meil mittepööratavad järeldusreeglid siduda järjestikuste valemitega.
Mõlemad vähendavad üldiselt tuletuskäikude arvu otsinguruumis.