Begreper & referanser
Alle nøkkelbegrepene, formlene og referansene fra Inferens i utsagnslogikk, samlet på én side. Bruk denne som oppslag når du leser, øver flashcards eller tar quiz.
Begreper
Sentrale begreper fra kapittelet med korte definisjoner.
Et mønster for å skrive en ny setning ut fra setninger som allerede står i beviset, som modus ponens. En sunn regel gir bare setninger som følger logisk av premissene (inference rule).
Inferensregelen som fra og gir . Den bruker implikasjonen framover, fra premiss til konklusjon (Modus Ponens).
Inferensregelen som fra og gir : er konklusjonen usann, kan ikke premisset være sant (Modus Tollens).
Inferensregelen som fra en konjunksjon gir hvert av leddene, og (And-Elimination).
Egenskapen at det som følger av en kunnskapsbase, fortsatt følger når nye setninger legges til: hvis , er også (monotonicity).
En formel skrevet som en konjunksjon av klausuler, som . Hver utsagnslogisk formel har en ekvivalent formel på denne formen (conjunctive normal form, CNF).
En disjunksjon av literaler, som . En klausul behandles som en mengde literaler, så rekkefølge og gjentakelser spiller ingen rolle (clause).
Et utsagnssymbol eller negasjonen av et, som eller . og er et komplementært par (literal).
Inferensregelen som fra to klausuler med et komplementært par literaler gir en ny klausul med alle de andre literalene. Brukt på er den fullstendig for utsagnslogikk (resolution).
Klausulen et resolusjonssteg gir: alle literalene fra de to foreldreklausulene unntatt det komplementære paret, med like literaler slått sammen (resolvent).
Klausulen uten literaler, skrevet □. Den kan aldri være sann, så når resolusjon finner den, er klausulmengden uoppfyllbar (empty clause).
En klausul med høyst én positiv literal, som , som kan skrives (Horn clause).
En klausul med nøyaktig én positiv literal. Den er enten et faktum som eller en regel (definite clause).
Datadrevet inferens over definitte klausuler: start i faktaene, bruk hver regel når alle premissene er kjent, og legg til konklusjonen, til spørringen er utledet eller ingenting nytt kommer (forward chaining).
Måldrevet inferens over definitte klausuler: start i spørringen og bevis premissene til en regel som har den som konklusjon, dybde først og fra venstre mot høyre (backward chaining).
En fullstendig, rekursiv algoritme som avgjør om en formel i CNF er oppfyllbar. Den bryter av tidlig, setter rene symboler og enhetsklausuler uten å forgrene, og forgrener ellers på ett symbol om gangen (Davis–Putnam–Logemann–Loveland).
En klausul der alle literalene unntatt én er usanne i modellen så langt, så den siste må være sann. Å sette den kan gi nye enhetsklausuler, og den kjeden heter enhetspropagering (unit clause, unit propagation).
Et symbol som har samme fortegn i alle klausulene som ikke allerede er sanne, for eksempel bare og aldri . DPLL setter det slik at literalene blir sanne (pure symbol).
Lokalt søk etter en modell: velg en usann klausul og snu med sannsynlighet et tilfeldig symbol i den, ellers symbolet som gjør flest klausuler sanne. Finner søket ingen modell, er det ikke et bevis for at formelen er uoppfyllbar (WalkSAT).
Formler
Hver formel: hva den heter, hvordan den ser ut, og hva symbolene betyr.
Resolusjonsregelen
Brukes i hvert resolusjonssteg. Resolver på nøyaktig ett komplementært par om gangen; har to klausuler to par, gir hvert av dem en tautologi, aldri □.
Slutningsmønsteret for modus ponens
Fra en implikasjon og premisset får du konklusjonen. Vanlig feil: å slutte fra og , som ikke er gyldig.
Lovene til De Morgan
Flytter inn i en parentes og bytter og . Brukes i steg 3 av CNF. Vanlig feil: å negere leddene uten å bytte konnektiv.
Distributivitet
Siste steg i CNF: distribuer over til ingen står inne i en . Vanlig feil: å stoppe før distribusjonen er fullført.
Bikondisjonal-eliminasjon
Første steg i CNF. Implikasjonene fjernes etterpå med implikasjonseliminasjon, så blir .
Kritisk forhold for tilfeldig 3-SAT
Med tilfeldige klausuler med tre literaler over symboler er nesten alle formler oppfyllbare når er klart under 4,26, og nesten ingen når det er klart over. De vanskeligste formlene ligger rundt overgangen.
Kodesnutter
Kodesnutter fra kapittelet, vist literal.
Fremoverkjeding med agenda og tellere
from collections import deque faktum_C = 1 # @param 0..1 # Definitte klausuler (premisser, konklusjon). Fakta har ingen premisser.regler = [(["A"], "B"), (["B", "C"], "D"), (["D", "E"], "Q"), (["A", "E"], "F"), (["F"], "G")]fakta = ["A", "E"] + (["C"] if faktum_C else []) teller = [len(set(p)) for p, _ in regler] # premisser igjen per regelagenda = deque(fakta) # FIFO-kø: fakta først, i oppgitt rekkefølgeutledet, fyrte = [], []bevist = Falsewhile agenda: p = agenda.popleft() if p in utledet: continue # allerede utledet: hopp over utledet.append(p) if p == "Q": bevist = True break for i, (premisser, konklusjon) in enumerate(regler): if p in premisser: teller[i] -= 1 if teller[i] == 0: agenda.append(konklusjon) fyrte.append(f"R{i + 1}") print(f"Utledet i rekkefølge: {', '.join(utledet)}")print(f"Regler som fyrte: {', '.join(fyrte) or 'ingen'}")print(f"Målet Q er bevist: {'ja' if bevist else 'nei'}")Prøv: sett faktum_C til 0 og se at Målet Q er bevist: blir nei, mens Utledet i rekkefølge: fortsatt får med B, F og G.
DPLL med og uten de to snarveiene
bruk_enhetsregel = 1 # @param 0..1bruk_rene_symboler = 1 # @param 0..1 # Hver klausul er en mengde literaler; "-B" betyr ¬B.klausuler = [{"D"}, {"-B", "-D"}, {"B", "D", "G"}, {"C", "G"}, {"C", "E"}, {"-C", "D", "F"}, {"-C", "D", "-G"}, {"D", "E", "-F"}]forgreninger = 0 def dpll(modell): global forgreninger aktive = [] # klausuler som ikke er sanne ennå, med de ukjente literalene for k in klausuler: if any(modell.get(l.lstrip("-")) == (l[0] != "-") for l in k): continue # klausulen er allerede sann rest = [l for l in k if l.lstrip("-") not in modell] if not rest: return None # alle literalene er usanne: gå tilbake aktive.append(rest) if not aktive: return modell lits = {l for k in aktive for l in k} if bruk_rene_symboler: for l in sorted(lits, key=lambda l: l.lstrip("-")): if (l[1:] if l[0] == "-" else "-" + l) not in lits: return dpll({**modell, l.lstrip("-"): l[0] != "-"}) if bruk_enhetsregel: for k in aktive: if len(k) == 1: return dpll({**modell, k[0].lstrip("-"): k[0][0] != "-"}) s = min(l.lstrip("-") for l in lits) # forgren på første symbol alfabetisk forgreninger += 1 m = dpll({**modell, s: True}) return m if m is not None else dpll({**modell, s: False}) m = dpll({}) # symboler som ikke står i modellen, kan ha hvilken som helst verdiprint(f"Oppfyllbar: {'ja' if m is not None else 'nei'}")if m is not None: print("Modell: " + ", ".join(f"{s} = {'sann' if v else 'usann'}" for s, v in sorted(m.items())))print(f"Antall forgreninger: {forgreninger}")Prøv: slå av bruk_enhetsregel og bruk_rene_symboler én om gangen og se hvordan Antall forgreninger: vokser fra 0, mens Oppfyllbar: er ja hele tiden.
Læringsmål
Hva du skal kunne etter å ha lest kapittelet.
- 01Avled en setning med nummererte linjer der hver linje oppgir regel og kildelinjer, med modus ponens, modus tollens, and-eliminasjon, and-introduksjon og disjunktiv syllogisme
- 02Bruk navngitte ekvivalenser som De Morgan, implikasjonseliminasjon og kontraposisjon, og navngi én omskriving per linje
- 03Konverter en utsagnslogisk formel til CNF med de fire stegene, og tell klausulene etter en oppgitt telleregel
- 04Bevis med resolusjon ved motsigelse ned til den tomme klausulen □
- 05Spor fremoverkjeding med agenda og tellere, og bakoverkjeding med målstabel, på definitte klausuler
- 06Forklar hvordan DPLL bruker tidlig avbrudd, rene symboler og enhetsklausuler, og hvorfor WalkSAT ikke kan bevise uoppfyllbarhet