Inferens i utsagnslogikk

Et adgangssystem har noen enkle regler. Stemmer PIN-koden ($P$), låses døra opp ($D$). I går kveld ble døra ikke låst opp, men hendelsen ble logget ($L$), og loggen viser at enten stemte PIN-koden, eller så tastet brukeren feil ($F$). Tastet brukeren feil? Du kan svare uten sannhetstabell ved å skrive nye setninger som følger av de gamle.

En inferensregel (inference rule) er et mønster for ett slikt steg. Den viktigste er modus ponens, og ƒslutningsmønsteret for modus ponens ser slik ut:

Over streken står premissene, under står det du får skrive. Fire regler til dekker de fleste bevis:

• •Med and-eliminasjon (And-Elimination) får du $\alpha$ og $\beta$ fra $\alpha \wedge \beta$.
• •Med and-introduksjon får du $\alpha \wedge \beta$ fra $\alpha$ og $\beta$ på hver sin linje.
• •Med modus tollens får du $\neg \alpha$ fra $\alpha \Rightarrow \beta$ og $\neg \beta$.
• •Med disjunktiv syllogisme, også kalt enhetsresolusjon, får du $\beta$ fra $\alpha \vee \beta$ og $\neg \alpha$.

Reglene er sunne: det de gir, følger logisk av premissene. Et bevis er nummererte linjer, og hver avledet linje oppgir regelen og numrene på linjene den bygger på, så sensor kan sjekke hvert steg for seg.

Å finne et bevis er et søkeproblem: en tilstand er linjene så langt, en handling er å bruke en regel, og målet er at setningen står på en linje. Søket kan overse symboler som ikke angår målet, og derfor er et bevis ofte mye kortere enn en sannhetstabell. Logikken er dessuten monoton, med monotonisitet (monotonicity): nye setninger i kunnskapsbasen gjør aldri en slutning ugyldig.

Inferensreglene brukes på hele linjer og bare i én retning. En logisk ekvivalens er sterkere: $\alpha \equiv \beta$ betyr at formlene er sanne i nøyaktig de samme modellene. Du kan derfor bytte den ene med den andre begge veier, og også inne i en større formel. Står $\neg (V\wedge O)\vee A$ på en linje, kan du skrive om bare parentesen med De Morgan.

Tabellen under har de samme navnene som formelarket på eksamen. To av dem bruker du hele tiden: ƒlovene til De Morgan flytter en negasjon inn i en parentes og bytter $\wedge$ og $\vee$, og ƒbikondisjonal-eliminasjon gjør $\iff$ om til to implikasjoner. Implikasjonseliminasjon, $\alpha \Rightarrow \beta \equiv \neg \alpha \vee \beta$, er broen mellom dem: med den kan du skrive enhver implikasjon som en disjunksjon.

I en avledning begrunnes en linje med en ekvivalens på samme måte som med en regel: «5. $\neg A\vee \neg V$, De Morgan fra 4». Navngi hver omskriving for seg. Skriver du to ekvivalenser på samme linje, kan ikke sensor se hvilken du brukte, og en feil i den ene gjør hele linja feil. Kontraposisjon står på arket, men den er ikke grunnleggende, for den følger av tre andre.

Resolusjon, som kommer i neste steg, virker bare på én bestemt form. En literal er et symbol eller negasjonen av et, som $K$ eller $\neg K$, der $K$ betyr at kortet i adgangssystemet er gyldig. En klausul (clause) er en disjunksjon av literaler, som $\neg K\vee \neg P\vee D$. En formel i konjunktiv normalform (conjunctive normal form, CNF) er en konjunksjon av klausuler. Hver utsagnslogisk formel kan skrives om til en ekvivalent CNF med fire steg i fast rekkefølge:

1. 1.Fjern $\iff$ med bikondisjonal-eliminasjon.
2. 2.Fjern $\Rightarrow$ med implikasjonseliminasjon.
3. 3.Flytt $\neg$ innover med De Morgan og dobbel negasjon, til $\neg$ bare står foran symboler.
4. 4.Distribuer $\vee$ over $\wedge$ med ƒdistributivitet, til ingen $\wedge$ står inne i en $\vee$.

Rekkefølgen er ikke tilfeldig. Steg 1 lager implikasjoner, som steg 2 fjerner. Steg 2 lager negasjoner foran parenteser, som steg 3 flytter inn. Og først når negasjonene sitter på symbolene, gir distribusjonen klausuler. Etter siste steg leser du av klausulene: hvert ledd i den ytterste konjunksjonen er én klausul. En klausul er en mengde literaler, så $D\vee D$ er bare $D$, og like klausuler telles én gang.

Et smarthus har en alarm $A$ som skal gå når vinduet $V$ står åpent og ovnen $O$ er av, og ellers ikke.

Disjunktiv syllogisme strøk én literal mot negasjonen sin. Regelen for resolusjon (resolution) gjør det samme med to hele klausuler. Har den ene klausulen en literal og den andre negasjonen av den, et komplementært par, får du en ny klausul med alle de andre literalene (ƒresolusjonsregelen):

Den nye klausulen heter en resolvent. $D$ står i den ene forelderen og $\neg D$ i den andre, og resten slås sammen. Står en literal i begge foreldrene, står den bare én gang i resolventen. Resolver alltid på nøyaktig ett komplementært par per steg.

Resolusjon brukes til bevis ved motsigelse. Du vil vise $KB\models \alpha$, og det er det samme som at $KB\wedge \neg \alpha$ er uoppfyllbar. Derfor:

1. 1.Gjør om KB og det negerte målet $\neg \alpha$ til klausuler.
2. 2.Resolver to og to klausuler og legg resolventene til.
3. 3.Får du en tom klausul (empty clause), □, er klausulmengden uoppfyllbar, og $KB\models \alpha$.

Den tomme klausulen kommer når to enhetsklausuler $X$ og $\neg X$ resolveres: ingen literaler er igjen, og en disjunksjon uten ledd kan aldri være sann. Gir ingen par flere nye resolventer uten at □ har dukket opp, følger ikke $\alpha$ av KB. Følger $\alpha$ av KB, finner resolusjonen □ før eller senere, så metoden er fullstendig.

I adgangssystemet betyr $K$ fortsatt at kortet er gyldig og $P$ at PIN-koden stemmer. Nå kan kortet også være sperret ($S$), og vi vil vise at hendelsen logges, $L$.

Resolusjon er fullstendig, men kan bli treg, fordi antallet mulige resolventer vokser fort. Mange kunnskapsbaser har en enklere form som gir raskere inferens. En Horn-klausul (Horn clause) har høyst én positiv literal. En definitt klausul (definite clause) har nøyaktig én og kan skrives som en regel: $\neg K\vee \neg P\vee D$ er det samme som $K\wedge P\Rightarrow D$. Et faktum som $P$ er en definitt klausul uten premisser. En Horn-klausul uten positiv literal, som $\neg A\vee \neg B$, er en begrensning: $A$ og $B$ kan ikke begge være sanne.

For definitte klausuler finnes en enkel og rask algoritme, fremoverkjeding (forward chaining). Den holder en agenda med symboler som er kjent sanne, og en teller per regel med antall premisser som ennå ikke er kjent:

1. 1.Legg faktaene i agendaen, i oppgitt rekkefølge.
2. 2.Ta ut det første symbolet. Er det spørringen, er du ferdig. Er det allerede utledet, hopper du over det.
3. 3.Ellers merker du det som utledet og teller ned hver regel som har det som premiss. Når en teller når 0, legges konklusjonen bakerst i agendaen.

Hvert symbol utledes høyst én gang, og hver regel fyrer høyst én gang, så tiden er lineær i størrelsen på KB. Algoritmen er sunn og fullstendig for definitte klausuler: hvert atom som følger av KB, blir utledet. Den er datadrevet, for den starter i det du vet, uten å vite hva du er ute etter. Modus ponens alene er bare fullstendig for Horn-KB-er; med klausuler som $A\vee B$ trengs resolusjon.

Tabellen viser fremoverkjeding i adgangssystemet: brikken leses ($B$), PIN-koden stemmer ($P$), det er nattmodus ($N$), og spørsmålet er om vaktsentralen varsles ($\text{Vakt}$). Agendaen er en kø, så $K$ må vente bak $P$ og $N$.

Fremoverkjeding utleder alt som følger, også det ingen har spurt om. Med bakoverkjeding (backward chaining) starter du i spørringen i stedet. For å bevise $\text{Vakt}$ finner algoritmen en regel med $\text{Vakt}$ som konklusjon og prøver å bevise premissene, ett og ett, på samme måte. Et faktum er bevist med en gang.

Arbeidet er et søk dybde først med en stabel av mål:

• •Ta det øverste målet av stabelen og prøv klausulene som har det som konklusjon, i oppgitt rekkefølge.
• •Premissene i en regel bevises fra venstre mot høyre.
• •Feiler et premiss, prøves neste regel for samme mål. Har ingen klausul målet som konklusjon, feiler det.
• •Står målet allerede på stien fra roten, feiler grenen. Uten den sjekken kan $A\Rightarrow B$ og $B\Rightarrow A$ gi en evig løkke.
• •Et mål som er bevist tidligere, trenger ikke bevises igjen.

Resultatet er et AND-OR-tre: en node er et mål, barna er premissene i regelen som brukes, og alle må bevises. Figuren viser treet for adgangssystemet fra forrige steg.

Bakoverkjeding er også sunn og fullstendig for definitte klausuler, med løkkesjekk. Den er måldrevet og rører bare regler som kan bidra til spørringen, og bruker ofte mye mindre tid enn størrelsen på KB tilsier. Fremoverkjeding passer når nye fakta kommer inn og du vil vite alt som følger; bakoverkjeding passer når du har ett spørsmål.

Mange problemer kan skrives som spørsmålet om en formel i CNF er oppfyllbar: timeplaner, kretser og sudoku. DPLL er en fullstendig algoritme for det. Den bygger en modell ett symbol om gangen og går tilbake ved konflikt, som backtracking i en CSP, men med tre forbedringer:

• •Tidlig avbrudd: en klausul er sann så snart én literal er sann, og formelen er usann så snart én klausul bare har usanne literaler. Du trenger ikke vente på en full modell.
• •Et rent symbol (pure symbol) har samme fortegn i alle klausulene som ikke er sanne ennå, og det settes slik at literalene blir sanne.
• •En enhetsklausul (unit clause) har bare én ukjent literal igjen, og resten er usanne, så den literalen må være sann. Én slik tilordning kan lage nye enhetsklausuler, og kjeden heter enhetspropagering.

Når ingen av reglene gjelder, forgrener DPLL: den setter et symbol til sann og prøver usann hvis det går galt.

WalkSAT går en helt annen vei. Den starter med en tilfeldig modell og velger en klausul som er usann. Med sannsynlighet $p$ snur den et tilfeldig symbol i klausulen, ellers symbolet som gjør flest klausuler sanne. Finner den en modell, er formelen oppfyllbar. Finner den ingen innen et fast antall snuinger, vet du ingenting: WalkSAT er ikke fullstendig og kan aldri bevise at en formel er uoppfyllbar. Til gjengjeld er den ofte mye raskere enn DPLL på store formler som har mange modeller. Med $p=0$ blir søket grådig og kan sette seg fast; med $p=1$ blir det en tilfeldig vandring.

Hvor vanskelig er en tilfeldig formel? For 3-SAT med $m$ klausuler over $n$ symboler avhenger svaret av ƒkritisk forhold for tilfeldig 3-SAT. Med få klausuler per symbol er nesten alle formler oppfyllbare, og en modell er lett å finne. Med mange er nesten ingen det, og det er også lett å slå fast. De vanskelige formlene ligger rundt overgangen.