Formal Logic: Classical Problems and Proofs
Logika je - nepochybne - celá o dokazovaní, ale dôkazy môžu byť "nákladné", často až nemožné, a dnes sa väčšina z nich deleguje na (čiastočne) automatické dokazovanie, konkrétne na takzvané SAT solvery, softvér založený na (boolovskom) probléme splniteľnosti alebo SAT. Ide o duálny problém (booleovskej) platnosti alebo VAL, ktorý je jadrom koncepcie digitálneho počítača prostredníctvom Hilbertovho Entscheidungsproblem a univerzálneho Turingovho stroja. Zatiaľ čo tieto problémy - VAL podstatne menej ako SAT - sa vyskytujú v úvodných učebniciach logiky určených študentom informatiky, v učebniciach určených študentom matematiky alebo filozofie zväčša alebo úplne chýbajú.
Formálna logika: Klasické problémy a dôkazy napravuje tento - podľa nášho názoru - nesprávny stav tým, že poskytuje základy formálnej klasickej logiky z ústredného pohľadu formálneho, resp. počítačového jazyka, ktorý sa od ostatných formálnych alebo počítačových jazykov odlišuje schopnosťou zachovávať pravdivosť, čím potenciálne poskytuje riešenia rozhodovacích problémov formulovaných v termínoch VAL a/alebo SAT. Tento základný aspekt klasickej logiky, zachovávanie pravdy, je rozpracovaný na základe troch hlavných formálnych sémantik, a to Tarského, Herbrandovej a algebraickej (booleovskej) sémantiky, ktoré sú zasa prostredníctvom výsledkov adekvátnosti pre štandardnú logiku prvého rádu základom hlavných dôkazových systémov priamych a nepriamych, resp. vyvracajúcich dôkazov, spojených s VAL a SAT.
Táto kniha nie je zameraná na dejiny klasickej logiky, ale napriek tomu poskytuje diskusie a cituje ústredné pasáže o jej vzniku a vývoji, a to z filozofického hľadiska. Keďže nejde o knihu z oblasti matematickej logiky, formálnu logiku berie z v podstate matematickej perspektívy. Priklonila sa k výpočtovému prístupu, ktorého základom sú SAT a VAL, a je teda úvodom do logiky, ktorý zahŕňa podstatné aspekty troch odvetví logiky, a to filozofickej, matematickej a výpočtovej.
