Logika u SAGE-u ⇨ implementacija funkcija

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.

Učitavanje gotovih paketa koji se koriste u implemetaciji dodatnih funkcija

In [1]:
import sage.logic.propcalc as logika
import sage.logic.logicparser as logikapar

Pomoćne funkcije

In [2]:
LATEX = lambda x: '$'+x.replace('<->','\\Leftrightarrow ').replace('->','\\Rightarrow ').replace('&','\\wedge ').replace('|','\\vee ').replace('~','\\neg ')+'$'
In [3]:
def bul(x):
    if bool(x)==True:
        return 1
    else:
        return 0
In [4]:
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()
In [5]:
def lijevo(t):
    if type(t)==list:
        return t[1]
    else:
        return t
In [6]:
def desno(t):
    if type(t)==list:
        return t[2]
    else:
        return t
In [7]:
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]
In [8]:
def zagrade(izraz):
    if len(izraz)>1:
        izraz='('+izraz+')'
    return  izraz
In [9]:
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

semanticka_tablica

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.

In [10]:
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'"

tablica_istinitosti

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).

In [11]:
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'"

Minimizacija

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.

Pomoćne funkcije

In [12]:
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)
In [13]:
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
In [14]:
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
In [15]:
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)
In [16]:
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)
In [17]:
def is_covered(cover,x):
    for k in range(len(cover)):
        if cover[k]!='-':
            if cover[k]!=x[k]:
                return 0
    return 1
In [18]:
def tablica_cover(lista):
    prosti=prosti_clanovi(lista)
    tablica=[[is_covered(x,y) for y in lista] for x in prosti]
    return tablica
In [19]:
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)
In [20]:
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
In [21]:
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
In [22]:
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]

Funkcije DNF, CNF, minDNF, minCNF

In [23]:
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)
In [24]:
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)
In [25]:
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))
In [26]:
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))
In [ ]: