Iti0210lab74

Resolutsioonimeetod

Sissejuhatus

Ülesande eesmärgiks on õppida, kuidas toimib resolutsioonimeetod.

Selleks:

1. programmeerime lihtsa versiooni resolutsioonil põhinevast tõestajast
2. testime seda ülesannete peal, kus on tarvis loogilist järeldamist

Lihtne resolutsioonil põhinev tõestaja

Teadaolevate faktide (KB) pealt mingi lause alpha tõestamiseks piisab, kui näidata et KB & -alpha on vastuolu, ehk siis ei ole võimalik korraga väita, et KB kehtib ja alpha ei kehti. Lihtne algoritmi prototüüp selleks:

def simple_resolution_solver(KB, neg_alpha):
    # KB: list of known clauses
    #           clause example: a v b v -c v d
    #           choose your own representation, e.g. ("a", "b", "-c", "d")
    # neg_alpha: query clause, already negated
    # returns True if proof found, False otherwise

    # initialize
    todo = [neg_alpha]
    done = KB.copy()

    # process the todo list one by one
    while todo:
        current = todo.pop()

        # combine current clause with all clauses we've already seen
        for clause in done:
            # apply resolution rule
            resolvents = resolve(current, clause)
            # handle new clauses generated by the resolution rule
            for resolvent in resolvents:
                # some important things that can happen here:
                # 1. resolvent is empty: proof found that KB->alpha!
                # 2. resolvent is always true: throw it away, useless clause
                # ONLY if neither of these things happen:
                    todo.append(resolvent)

        # we're done with this clause
        done.append(current)

    # loop ended without proof
    return False

Funktsioon resolve(current, clause) peab tagastama listi võimalikest tulemustest, mida saadakse kahele disjunktile current ja clause resolutsioonireegli rakendamisel. See funktsioon kirjuta ise.

resolve() näited

Katsetame seda algoritmi väikese ülesande peal:

  P -> Q
  L & M -> P
  B & L -> M
  A & P -> L
  A & B -> L
  A
  B

Tõesta, et nende reeglite ja faktide pealt järeldub Q. Selleks pead reeglid kõigepealt CNF kujule viima, näiteks L & M -> P teisendub -L v -M v P. Funktsioonile pead tõestatava asja ette andma eitusena (-Q). Pane tähele, et tõestatav asi on ka disjunkt/lause, isegi kui ta koosneb ainult ühest literaalist.

Teooria: ANL loop, set of support

Toodud algoritm on küll lihtne, aga sisaldab juba õpiku kirjeldusega võrreldes olulisi optimisatsioone:

1. "ANL loop" on algoritm, kus disjunktid jaotatakse "tegemata" ja "tehtud" listideks. Disjunkte võetakse ükshaaval tegemata listist ning proovitakse resolutsioonireeglit selle ja kõigi tehtud listi disjunktide vahel. Tekkinud uued disjunktid lisatakse tegemata listi. See garanteerib, et sama paari ei vaadata mitu korda.
2. Set of support strateegia: kuna meil on eesmärgiks mingi fakti järeldumist kontrollida, siis see strateegia paneb "tegemata" listi ainult kontrollitava fakti ja "tehtud" listi kogu ülejäänud teadmise. Tegemata listi hakkavad siis tekkima ainult asjad, mis on kuidagi seotud meie kontrollitava faktiga. Näiteks, testülesande puhul on tegemata listis -Q ja kõik faktid tehtud listis, esimeses tsüklis tekiks kohe -P mis tähendab, et Q tõestamiseks peame esmalt tõestama P. Järgmisena leitakse P eeldused jne - see on väga sarnane backward chaining algoritmiga.

Optimeeritud variant

Esialgne variant järeldusmootorist küll töötab, aga kui ta kohe järeldust ei leia, hakkab resolutsioonireegel piiramatult uusi disjunkte genereerima - proovi näiteks eemaldada testülesandest Q tõestamiseks vajalik fakt A ja vaata mis juhtub.

Lisame neeldumise kontrolli. Lihtsustatult öeldes kontrollitakse iga resolutsioonireegli poolt genereeritud disjunkti juures, kas oli juba enne olemas mingi disjunkt, mis sisaldab sama infot.

def resolution_solver(KB, neg_alpha):
    # KB: list of known clauses
    #           clause example: a v b v -c v d
    #           choose your own representation, e.g. ("a", "b", "-c", "d")
    # neg_alpha: query clause, already negated
    # returns True if proof found, False otherwise

    # initialize
    todo = [neg_alpha]
    done = KB.copy()

    # process the todo list one by one
    while todo:
        current = todo.pop()

        # check if current is redundant
        for clause in done + todo:
            # if clause is a subset of current, then go back to the start of the loop
            # to pick new current

        # combine current clause with all clauses we've already seen
        for clause in done:
            # apply resolution rule
            resolvents = resolve(current, clause)
            # handle new clauses generated by the resolution rule
            for resolvent in resolvents:
                # some important things that can happen here:
                # 1. resolvent is empty: proof found that KB->alpha!
                # 2. resolvent is always true: throw it away, useless clause
                # ONLY if neither of these things happen:
                    todo.append(resolvent)

        # we're done with this clause
        done.append(current)

    # loop ended without proof
    return False

Nüüd peaks algoritm kiiresti tulemusi andma, kui tõestust ei leita. Proovi jälle testülesannet, eemaldades fakti A või vajaliku reegli A & B -> L.

Teooria: neeldumine

Kui meil on disjunktid A v B v C v D ja A v B v C, siis neist esimese võib ära jätta - miks, seda saab hästi aru lühema näite pealt: a & (a v b) on ekvivalentne a-ga. Resolutsioonimeetodi kontekstis nimetatakse seda tehnikat subsumption, ehk neeldumine. Kui kontrollime neeldumist nii, et leiame kas üks disjunkt on teise alamhulk, siis sellega leitakse ka korduvad disjunktid.

Ülesanne lahendamiseks

Meil on antud maja elektriskeem, kus on kaitsmed (cb), seinakontaktid (p), lambid (l), lülitid (s) ja juhtmed (w). Valime iga elemendi - juhtme, kaitsme jne kohta ühe loogikasümboli ning ütleme, et kui näiteks w1 on tõene, siis juhtmes 1 on vool. Lepime kokku, et elektriskeem töötab nii:

1. vool läbib kaitsmeid, kui need on korras (näiteks cb1 on tõene). Lülitite puhul tähistab tõene ülemist asendit ja väär alumist asendit, skeemilt on näha kuidas vool neid sel juhul läbib.
2. kui juhtmes on vool, siis sellega otse ühendatud lamp põleb (ja vastupidi, põleva lambi puhul on vool juhtmes).
3. kui juhtmes on vool, siis selle küljes olevas seinakontaktis on vool - sama kehtib ka vastupidises suunas.
4. juhul kui kaks juhet on omavahel lüliti või töötava kaitsmega ning ühes pole voolu, ei saa ka teises olla voolu.
5. kui lamp on kustu või seinakontaktis pole voolu, siis ei saa ka nende küljes olevas juhtmes olla voolu.

(pilt (c) D. Poole, A. Mackworth; [1])

Küsimused testimiseks

1. Väline vool on olemas (outside_power) ning kaitse 2 on korras (cb2). Tõesta, et pistikus p2 on vool.
2. Väline vool on, kaitse 1 (cb1) on korras. Lüliti 1 (s1) on alumises asendis ja lüliti 2 (s2) ülemises asendis. Tõesta, et lamp l1 ei põle.
3. Väline vool on olemas, lülitid s1 ja s2 on samas asendis, näiteks ülemises. Lamp l1 ei põle. Tõesta, et kaitse 1 (cb1) on katki/välja lülitunud.

Meil tuleb teha:

• reeglid, mis kirjeldavad, kuidas elektriskeem töötab
• faktid (iga küsimuse kohta eraldi).
• lause, mida hakatakse tõestama (tõestajale ette anda vastasmärgiga).

Kuna reeglid peavad olema KNK (CNF) kujul, siis kasuta vajaduse korral teisendamiseks http://logictools.org/prop.html - nupp "Build" ja vali kõrvalt "clause normal form".

Esitamine

Kui oled tõestustega hakkama saanud, siis README failis esita:

1. iga küsimuse juurde tehtud faktid, mis kirjeldavad antud situatsiooni
2. näide mõnest keerulisemast reeglist, võib olla nii algkujul kui KNK kujul. Kõiki reegleid pole tarvis tuua.