|
|
Metode za odredjivanje tautologija
Osim metoda tablice istinitosti i redukcije na apsurd razradjene su i druge metode koje zavisno od načina primene imaju svoje prednosti i nedostnedostatke. Zbog odlučnosti iskaznog računa, dokaz da je data formula teorema(u sintaksnom smislu),odnosno tautologija(u semantičkom smislu),može se svesti na ispitivanje odgovarajućeg kriterijuma.Postoje razni kriterijumi i razni postupci za njihovu proveru.Aritmetička metoda je zasnovana na numeričkom kriterijumu i aritmetičkom postupku za njegovu proveru.Algebarska metoda je zasnovana na algebarskim svojstvima logičkih operacija i na vezama sa osnovnim aritmetičkim operacijama.
Aritmtička metoda: U vezi sa svakom iskaznom formulom F(p1,p2,...,pn), gde su p1,...,pn iskazna slova uvodi se izraz f(k1,...,kn), gde su brojevi 
F(p1,...,pn) je tautologija ako važi f(k1,...,kn)=I(n) Prilikom izračunavanja vrednosti f(k1,...,kn) služimo se jednakostima :
'not'x = I(n) - x
x∨y=x+y-x∧y=x+'not'x∧y
x=>y='not'x+x∧y
x<=>y='not'x∧'not'y+x∧y='not'(x+y)+2(x∧y)
Gde su x,y∈{0,1,...,I(n)}, a +,-,o su obične aritmetičke operacije. Za izvršavanje operacije ∧ na skupu {0,1,...,I(n)},dovoljno je imati tablicu ove operacije. Neka matrica T2m odredjuje sadržaj tablice konjunkcije na skupu 
={0,1,...,
} i neka je K2m kvadratna matrica reda 
tada:
T1=[0] m=0,1,...,
Algebarska metoda: Ova metoda zasniva se na sledećim vezama logičkih i aritmetičkih operacija na L2={0,1}:
'not'y=1-x
x∧y=xy
x∨y=x+y-xy (*)
x=>y=1-x+xy
x<=>y=1-(x+y)+2xy
Na identitetu n:x za n∈N i x∈L2 važi sledeći kriterijum: F(p1,...,pn) je tautologija akko algebarski izraz pridružen ovoj formuli na osnovu veza (*), identički je jednak 1.
Rezolucijska metoda opovrgavanja: Za iskazni račun pravilo rezolucije može se zapisati u sledećem obliku:
( R ) 
,gde su A,B,C iskayne formule. Pravilo rezolucije primenjuje se na sastavke. Sastavci su disjunkcije raznih slova ili njihovih negacija. Za odredjivanje skupa sastavaka data formula se transformiše u konjunktivnu normalnu formu. Ta metoda zasniva se na sledećem stavu potpunosti pravila rezolucije: F(p1,...,pn) je tautologija akko konačnom primenom pravila rezolucije na polazni skup sastavaka, odradjen iz negacije date formule, izvodi se kontradikcija.