interpretatsioonis valemite vabade muutujate kõikidel väärtustel. 6 Ülesandeid konspektis ei vaatle 9 Prefikskuju. Valemi prefikskujule viimise algoritm. Ütleme, et valem F on prefikskujul, kui F = Q1x1Q2x2 . . . QnxnF, kus Q1, Q2, . . . , Qn on kvantorid, x1, x2, . . . , xn indiviidmuutujad ja F kvantoriteta valem. Prefikskuju on lähtekoht paljudele predikaatarvutuse algoritmidele, ta mängib predikaatarvutuses sarnast rolli nagu TDNK ja TKNK lausearvutuses Teisendamise algoritm: Olgu antud valem F. 1) Elimineerida implikatsioonid ja ekvivalentsid. 2) Viia eitused kvantorite alla. Kahekordsed eitused jätta ära. 3) Nimetada seotud muutujad ümber nii, et iga kvantor seoks erinevat muutujat ja et ükski kvantor ei seoks muutujat, mis esineb kuskil vabalt. 4) Tuua kvantorid valemi ette.
parajasti siis, kui kandjas on n elementi, ja saab konstrueerida kehtestatava valemi, mis on väär igas lõpliku kandjaga interpretatsioonis Kui signatuur on lõplik või loenduv, siis loenduvast suuremate kandjate vaatlemine pole vajalik t on juba olemasolev sisse toodud tähis ja c on uus konstant, mis tuuakse sisse Ütleme, et valem F on prefikskujul, kui F = Q1x1Q2x2 ... QnxnF , kus Q1, Q2, ... , Qn on kvantorid, x1, x2, ... , xn indiviidmuutujad ja F kvantoriteta valem, mida nimetatakse valemi F maatriksiks o Prefikskujule viimise algoritm: Avaldame implikatsiooni ja ekvivalentsi teiste tehete kaudu Viime eitused kvantorite alla Nimetame ümber seotud muutujad Toome kõik kvantorid sulgude ette 4. TÕESTUSTAKTIKAD Teoreemi üldkuju: kui on täidetud eeldused E1, ..., Ne, siis kehtib väide V Väide on kujul B&C Eeldus on kujul B&C Väide on kujul BvC
annaabi.ee 
