U ovom dijelu je cilj implementirati dvije dodatne funkcije semanticka_tablica i tablica_istinitosti čije svrhe su opisane kasnije. Pritom definiramo niz pomoćnih funkcija koje nam pomažu u implementaciji spomenutih funkcija. Pomoćne funkcije rade određene zahtjevne tehničke poslove čiji rezultati su od velike važnosti u implementaciji funkcija semanticka_tablica i tablica_istinitosti. Rezultati pomoćnih funkcija u većini slučajeva nisu od nekog posebnog interesa pa pomoćne funkcije pojedinačno nisu detaljno objašnjene. No, svatko za sebe može detaljnije proći implementaciju svake od pomoćnih funkcija i zaključiti što pojedina pomoćna funkcija radi.
Sve implementirane funkcije možete koristiti u svojem notebooku tako da učitate datoteku logika.sage.
import sage.logic.propcalc as logika
import sage.logic.logicparser as logikapar
LATEX = lambda x: '$'+x.replace('<->','\\Leftrightarrow ').replace('->','\\Rightarrow ').replace('&','\\wedge ').replace('|','\\vee ').replace('~','\\neg ')+'$'
def bul(x):
if bool(x)==True:
return 1
else:
return 0
def tablica_ispis(lista,stupac):
lista=list(map(list,list(lista)))
lista2=list(map(list, zip(*lista)))
ds=list(map(lambda x: len(str(max(x))),lista2))
ds2=list(map(lambda x: len(str(x)),stupac))
duljine_stupaca=list(map(max,zip(ds,ds2)))
broj_crtica='-'*(sum(duljine_stupaca)+len(duljine_stupaca)-1)
for k in range(len(stupac)):
print(str(stupac[k]).center(duljine_stupaca[k]), end = ' ')
print()
print(broj_crtica)
for element in lista:
for k in range(len(element)):
print(str(element[k]).center(duljine_stupaca[k]), end = ' ')
if element!=lista[-1]: print()
def lijevo(t):
if type(t)==list:
return t[1]
else:
return t
def desno(t):
if type(t)==list:
return t[2]
else:
return t
def postorder(t):
if type(t)!=list:
yield t
else:
for x in postorder(lijevo(t)):
yield x
for x in postorder(desno(t)):
yield x
yield t[0]
def zagrade(izraz):
if len(izraz)>1:
izraz='('+izraz+')'
return izraz
def komadi(t):
lista=list(postorder(t))
operacije=['~','&','|','->','<->']
stog=[]
dio=[]
for x in lista:
if not(x in operacije):
stog.append(x)
else:
a=stog.pop()
b=stog.pop()
if x=='~':
izraz=x+b
else:
izraz=zagrade(b)+x+zagrade(a)
stog.append(izraz)
dio.append(izraz)
return dio
Funkcija semanticka_tablica daje na izlazu semanticku tablicu zadane formule logike sudova. Formula se zadaje u obliku stringa, a podržane su sljedeće operacije:
| negacija | ~ |
| konjunkcija | & |
| disjunkcija | | |
| implikacija | -> |
| ekvivalencija | <-> |
Automatski se određuju svi dijelovi zadane formule i za svaki takav dio se formira stupac u tablici na izlazu. Opcija izlaz po defaultu ima vrijednost "tablica", što znači da će se na izlazu ispisati semantička tablica. Ukoliko je izlaz="rjecnik", tada će se semantička tablica ispisati u obliku rječnika. To može biti korisno u slučaju da je semantička tablica velika pa može doći do nepreglednog vizualnog ispisa tablice ukoliko bi bilo izlaz="tablica". Treća opcija je izlaz="html" koji daje vizualno lijepu i oku ugodnu tablicu pri čemu formule renderira MathJax tako da procesira LaTeX kod tih formula.
def semanticka_tablica(formula,izlaz="tablica"):
dijelovi1=sorted(logikapar.parse(formula)[1])
dijelovi2=komadi(logikapar.parse(formula)[0])
dijelovi3=map(lambda x: logika.formula(x), dijelovi2)
tabl=logika.formula(formula).truthtable().get_table_list()[1:]
tablica=list(reversed(list(map(lambda x: x[0:-1], tabl))))
for x in dijelovi3:
for k in range(len(tablica)):
vrijednost=x.evaluate(dict(zip(dijelovi1,tablica[k][0:len(dijelovi1)])))
tablica[k].append(vrijednost)
tablica=list(map(lambda x: list(map(bul,x)), tablica))
if izlaz=="tablica":
return tablica_ispis(tablica,dijelovi1+dijelovi2)
elif izlaz=="rjecnik":
tablica=list(map(list,zip(*tablica)))
return dict(zip(dijelovi1+dijelovi2,tablica))
elif izlaz=="html":
dijelovi1 = list(map(LATEX, dijelovi1))
dijelovi2 = list(map(LATEX, dijelovi2))
hed=dijelovi1+dijelovi2
return table([hed]+tablica)
else:
return "Error: varijabla 'izlaz' mora imati jednu od tri vrijednosti 'tablica', 'rjecnik' ili 'html'"
Funkcija tablica_istinitosti daje na izlazu tablicu istinitosti svih formula koje su navedene u listi formule. Formule se zadaju na isti način kao i kod funkcije semanticka_tablica. U ovom slučaju se daje samo tablica istinitosti samih formula, ali ne i njihovih manjih dijelova (osim ako nisu zasebno navedeni u listi formule).
def tablica_istinitosti(formule,izlaz="tablica"):
varijable=[]
for x in formule:
varijable.extend(logikapar.parse(x)[1])
varijable=sorted(list(Set(varijable)))
tablica=sorted(list(Tuples([True,False],len(varijable))),reverse=True)
for x in formule:
for k in range(len(tablica)):
vrijednost=logika.formula(x).evaluate(dict(zip(varijable,tablica[k][0:len(varijable)])))
tablica[k].append(vrijednost)
tablica=list(map(lambda x: list(map(bul,x)),tablica))
if izlaz=="tablica":
return tablica_ispis(tablica,varijable+formule)
elif izlaz=="html":
varijable = list(map(LATEX, varijable))
formule = list(map(LATEX, formule))
return table([varijable+formule]+tablica)
else:
return "Error: varijabla 'izlaz' mora imati jednu od dvije vrijednosti 'tablica' ili 'html'"
U ovom dijelu su implementirane četiri funkcije DNF, CNF, minDNF i minCNF koje za danu formulu logike sudova daju njezinu disjunktivnu i konjunktivnu normalnu formu te minimizacije tih formi. Za minimizaciju je implementiran Quine–McCluskey algoritam koji ima eksponencijalnu složenost s obzirom na broj varijabli u formuli. Međutim, za mali broj varijabli (do desetak varijabli) on dobro funkcionira. U postizanju tog cilja implementiran je niz pomoćnih funkcija koje nećemo posebno objašnjavati, niti pak su one same za sebe od nekog većeg interesa.
def izlaziF(formula,bit=1):
varijable=sorted(logikapar.parse(formula)[1])
tablica=sorted(list(Tuples([True,False],len(varijable))),reverse=True)
out=[]
for k in range(len(tablica)):
vrijednost=logika.formula(formula).evaluate(dict(zip(varijable,tablica[k])))
if vrijednost==bit: out.append(tablica[k])
out=list(map(lambda x: ''.join(x), map(lambda x: map(str,map(bul,x)), out)))
return(out)
def broj_jedinica(lista):
rjecnik={}
for elem in lista:
broj1=elem.count('1')
if broj1 in rjecnik:
rjecnik[broj1].append(elem)
else:
rjecnik[broj1]=[elem]
return rjecnik
def usporedi(x,y):
razliciti=0
for k in range(len(x)):
if x[k]!=y[k]:
razliciti+=1
if razliciti>1:
return False
else:
x1=x[0:k]+'-'+x[k+1:]
return x1
def novi_stupac(rjecnik):
lista=[]
nisu_prosti=set([])
for k in rjecnik:
if k+1 in rjecnik:
for x in rjecnik[k]:
for y in rjecnik[k+1]:
if usporedi(x,y):
lista.append(usporedi(x,y))
nisu_prosti.update(set([x,y]))
svi=[]
for elem in rjecnik.values():
svi=svi+elem
prosti=set(svi).difference(nisu_prosti)
return (broj_jedinica(list(set(lista))),prosti)
def prosti_clanovi(lista):
rjecnik=broj_jedinica(lista)
prosti=set([])
while rjecnik!={}:
a=novi_stupac(rjecnik)
prosti.update(a[1])
rjecnik=a[0]
return list(prosti)
def is_covered(cover,x):
for k in range(len(cover)):
if cover[k]!='-':
if cover[k]!=x[k]:
return 0
return 1
def tablica_cover(lista):
prosti=prosti_clanovi(lista)
tablica=[[is_covered(x,y) for y in lista] for x in prosti]
return tablica
def bitni_prosti(lista):
prosti=prosti_clanovi(lista)
tablica=tablica_cover(lista)
tablica1=list(map(list, zip(*tablica)))
prosti2=[]
indeksi=[]
for x in tablica1:
jedinice=0
for y in x:
if y==1:
jedinice+=1
if jedinice>1:
break
else:
ind=x.index(y)
if jedinice==1:
prosti2.append(prosti[ind])
indeksi.append(ind)
for i in set(indeksi):
for k in range(len(tablica[i])):
if tablica[i][k]!=0:
for k1 in range(len(tablica1[k])):
tablica1[k][k1]=0
tablica1= list(map(list, zip(*tablica1)))
return (list(set(prosti2)),list(set(indeksi)),tablica1)
def is_nulmatrica(matrica):
m=len(matrica)
n=len(matrica[0])
for i in range(m):
for j in range(n):
if matrica[i][j]!=0:
return False
return True
def minDNF_internal(formula,bit=1):
lista=izlaziF(formula,bit)
rj=bitni_prosti(lista)
prostiClanovi=prosti_clanovi(lista)
prosti_cover=rj[0]
indeksi=rj[1]
M=0
matrica=rj[2]
while not(is_nulmatrica(matrica)):
for k in range(len(matrica)):
if not(k in indeksi):
if matrica[k].count(1)>M:
M=matrica[k].count(1)
ind=k
indeksi.append(ind)
prosti_cover.append(prostiClanovi[ind])
for j in range(len(matrica[ind])):
if matrica[ind][j]!=0:
for t in range(len(matrica[ind])):
matrica[t][j]=0
return prosti_cover
def convert_to_znakovi(kod,znakovi,operacija='&'):
rijec=''
if operacija=='&':
for k in range(len(kod)):
if kod[k]=='1': rijec=rijec+znakovi[k]+operacija
if kod[k]=='0': rijec=rijec+'~'+znakovi[k]+operacija
elif operacija=='|':
for k in range(len(kod)):
if kod[k]=='0': rijec=rijec+znakovi[k]+operacija
if kod[k]=='1': rijec=rijec+'~'+znakovi[k]+operacija
return rijec[:-1]
def DNF(formula):
if not(logika.formula(formula).is_contradiction()):
varijable=sorted(logikapar.parse(formula)[1])
dnf=izlaziF(formula,1)
dnf=list(map(lambda x: convert_to_znakovi(x,varijable), dnf))
dnf=list(map(lambda x: '('+x+')' if len(x)>2 else x, dnf))
ispis='|'.join(dnf)
return show(logika.formula(ispis))
else:
return show(0)
def CNF(formula):
if not(logika.formula(formula).is_tautology()):
varijable=sorted(logikapar.parse(formula)[1])
cnf=izlaziF(formula,0)
cnf=list(map(lambda x: convert_to_znakovi(x,varijable,'|'), cnf))
cnf=list(map(lambda x: '('+x+')' if len(x)>2 else x, cnf))
ispis='&'.join(cnf)
return show(logika.formula(ispis))
else:
return show(1)
def minDNF(formula):
if logika.formula(formula).is_contradiction():
return show(0)
elif logika.formula(formula).is_tautology():
return show(1)
else:
varijable=sorted(logikapar.parse(formula)[1])
dnf=minDNF_internal(formula)
dnf=list(map(lambda x: convert_to_znakovi(x,varijable), dnf))
dnf=list(map(lambda x: '('+x+')' if len(x)>2 else x, dnf))
ispis='|'.join(dnf)
return show(logika.formula(ispis))
def minCNF(formula):
if logika.formula(formula).is_contradiction():
return show(0)
elif logika.formula(formula).is_tautology():
return show(1)
else:
varijable=sorted(logikapar.parse(formula)[1])
cnf=minDNF_internal(formula,0)
cnf=list(map(lambda x: convert_to_znakovi(x,varijable,'|'), cnf))
cnf=list(map(lambda x: '('+x+')' if len(x)>2 else x, cnf))
ispis='&'.join(cnf)
return show(logika.formula(ispis))