Tõestuseotsingu 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 see kehtib igal 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 otsingul mitte-determineeritust.
- Esimene neist kasutab 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.

1. Pööramine (ppt)
   
2. Fokuseerimine (ppt)