vabade muutujate kõikidel väärtustel, kus valemid 1 , 2 , ... , on tõesed, on ka valem G tõene · Valemid F ja G nim samaväärseteks, kui nende tõeväärtused on võrdsed igas 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.
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 Eeldus on kujul BvC Väide on kujul B->C Eeldus on kujul B->C
annaabi.ee 
