Inferens i førsteordens logikk

Den enkleste måten å resonnere i førsteordens logikk på er å gjøre alt om til utsagnslogikk og bruke metodene fra forrige kapittel. To inferensregler fjerner kvantorene.

Med universell instansiering (Universal Instantiation, UI) gjelder det som gjelder for alle, for hver enkelt. Regelen er ƒregelen for universell instansiering:

Her er $g$ en grunnterm, en term uten variabler, og regelen kan brukes så mange ganger du vil. Fra $\forall x(\text{Medlem}(x)\Rightarrow \text{Betalt}(x))$ får du $\text{Medlem}(\text{Ane})\Rightarrow \text{Betalt}(\text{Ane})$, og like gjerne $\text{Medlem}(\text{Mor}(\text{Bo}))\Rightarrow \text{Betalt}(\text{Mor}(\text{Bo}))$.

Med eksistensiell instansiering (Existential Instantiation, EI) er regelen strengere, se ƒregelen for eksistensiell instansiering. Fra $\exists y\text{Glemte}(y,\text{Kart})$ vet du at noen glemte kartet, men ikke hvem. Du kan gi personen et nytt navn, $\text{Glemte}(C_1,\text{Kart})$, men navnet må være nytt. Skriver du $\text{Glemte}(\text{Ane},\text{Kart})$, påstår du noe KB aldri sa. Regelen brukes én gang for hver setning med $\exists$. Den nye KB-en er ikke ekvivalent med den gamle, men den er oppfyllbar nøyaktig når den gamle er det, og det er nok for bevis ved motsigelse.

Ved propositionalisering (propositionalization) brukes UI med alle grunntermer og EI på alle setninger med $\exists$. Uten funksjonssymboler er det endelig mange grunntermer, og resultatet er en vanlig utsagnslogisk KB. Med en funksjon som $\text{Mor}$ finnes uendelig mange: $\text{Ane}$, $\text{Mor}(\text{Ane})$, $\text{Mor}(\text{Mor}(\text{Ane}))$ og så videre. Følger en setning av KB, finnes et bevis med termer opp til en viss dybde, så du finner det ved å lete dybde for dybde. Følger den ikke, tar letingen aldri slutt: logisk konsekvens i FOL er semi-avgjørbar.

Selv uten funksjoner blir propositionaliseringen fort stor. Et predikat med $k$ argumenter og $p$ konstanter gir $p^k$ grunne atomer, og en regel med tre variabler instansieres på $p^3$ måter, selv om bare én av dem trengs for å svare på spørsmålet. Resten av kapitlet handler om å slippe det arbeidet ved å la variablene stå til vi vet hvilke verdier som trengs.

Propositionalisering lager mange setninger som aldri brukes. Det er bedre å la reglene stå med variabler og finne verdiene som trengs. Ved unifisering (unification) finner du en substitusjon (substitution) θ som gjør to uttrykk like (ƒdefinisjonen av UNIFY):

Ta $p=\text{Gikk}(\text{Ane},t)$ og $q=\text{Gikk}(x,\text{Gausta})$. Da er $\text{UNIFY}(p,q)=\{x/\text{Ane},t/\text{Gausta}\}$, og begge blir $\text{Gikk}(\text{Ane},\text{Gausta})$. Algoritmen går gjennom argumentene parvis fra venstre og bygger opp θ:

• •To like konstanter passer. To ulike konstanter feiler.
• •En variabel mot en term gir en binding. Er variabelen alt bundet, sammenlignes verdien i stedet.
• •To sammensatte termer med samme funksjon og like mange argumenter sammenlignes argument for argument.

Ofte finnes mange unifikatorer. For $\text{Gikk}(\text{Ane},t)$ og $\text{Gikk}(x,u)$ er $\{x/\text{Ane},t/u\}$ nok, mens $\{x/\text{Ane},t/\text{Gausta},u/\text{Gausta}\}$ også gjør dem like, men låser turen uten grunn. Vi vil ha den mest generelle unifikator (most general unifier, MGU), som binder minst mulig. Komponert form, der ingen verdi inneholder en variabel som selv er bundet, er standard: $\{y/\text{Ane},w/\text{Mor}(\text{Ane})\}$. Den triangulære $\{y/\text{Ane},w/\text{Mor}(y)\}$ godtas når oppgaven ikke ber om komponert form.

MGU-en er entydig opp til navn på variabler: binder én algoritme $x/y$ og en annen $y/x$, er resultatene like gode. Skal du vise unifiseringen for hånd, skriv én linje per sammenligning: hva som sammenlignes, hvilken binding det gir, og θ så langt. Da ser sensor hvor en feil eventuelt kom inn, og hvorfor unifiseringen stopper når den gjør det.

Én regel til stopper uendelige termer. Med occurs check (occurs check) nekter algoritmen å binde en variabel til en term der variabelen selv står: $x$ mot $\text{Mor}(x)$ har ingen unifikator, fordi $x$ da måtte vært $\text{Mor}(\text{Mor}(\text{Mor}(\dots )))$. Sjekken koster tid, fordi hele termen må gjennomsøkes for hver binding, og noen systemer hopper over den for å gå raskere. Da kan et bevis «lykkes» på grunnlag av en term som ikke finnes.

Parene under unifiseres hver for seg.

Med unifisering kan modus ponens brukes direkte på regler med variabler. Regelen generalisert modus ponens (Generalized Modus Ponens, GMP) tar fakta $p_1^{\prime },\dots ,p_n^{\prime }$ og en regel $p_1\wedge \cdots \wedge p_n\Rightarrow q$ (ƒregelen for generalisert modus ponens):

der én og samme θ gjør $\text{SUBST}(\theta ,p_i^{\prime })=\text{SUBST}(\theta ,p_i)$ for alle $i$. Du unifiserer premissene ett og ett, og hver binding følger med til neste. Når alle passer, bruker du θ på konklusjonen.

Regelen er sunn. Alle setningene i KB er universelt kvantifisert, så universell instansiering med θ gir $\text{SUBST}(\theta ,p_i^{\prime })$ og $\text{SUBST}(\theta ,p_1\wedge \cdots \wedge p_n\Rightarrow q)$. Siden θ gjør hvert faktum likt det tilhørende premisset, gir vanlig modus ponens $\text{SUBST}(\theta ,q)$. GMP gjør altså de samme stegene, bare uten å skrive ut alle instansieringene.

Generalisert modus ponens er et eksempel på løfting (lifting): en utsagnslogisk regel gjort om til en førsteordens regel med variabler. Den gjør bare de instansieringene som faktisk trengs, og derfor er den så mye raskere enn propositionalisering.

Før unifiseringen får variablene i regelen og i hvert faktum egne navn, ved standardisering av variabler (standardizing apart). Hver setning er kvantifisert for seg, så $x$ i regelen og $x$ i et faktum er to ulike variabler. Får de samme navn, kan en binding fra regelen krasje med faktumet.

Turlaget gir merke for hver fjelltur et medlem fullfører.

Fremoverkjeding virker som i utsagnslogikk, men en regel kan fyre med mange ulike θ. I hver iterasjon prøves hver regel mot alle fakta som er kjent ved starten av iterasjonen, og hver θ som passer, gir et nytt faktum. Nye fakta legges til etter iterasjonen, og søket stopper når spørringen er utledet eller ingenting nytt kommer, ved et fikspunkt. Fremoverkjeding er sunn og fullstendig for førsteordens definitte klausuler: følger $q$, finner den $q$.

For datalog (Datalog), definitte klausuler uten funksjonssymboler, finnes bare endelig mange grunne atomer, så fremoverkjedingen stopper alltid. Med funksjonssymboler kan den fortsette for alltid når $q$ ikke følger: $\text{Tall}(x)\Rightarrow \text{Tall}(S(x))$ gir et nytt faktum i hver iterasjon.

maks_iterasjoner = 5  # @param 1..5
# Utskrift: én linje «Iterasjon <k>: …» per iterasjon og til slutt «Nye fakta totalt: …».

# Sti(a, b): det går en merket sti fra hytte a til hytte b.
fakta = {("Sti", "A", "B"), ("Sti", "B", "C"), ("Sti", "C", "D"), ("Sti", "D", "E")}
# Datalog-regler (premisser, konklusjon); variabler er små bokstaver.
regler = [([("Sti", "x", "y")], ("Naar", "x", "y")),
          ([("Sti", "x", "y"), ("Naar", "y", "z")], ("Naar", "x", "z"))]

def match(premisser, theta, kjente):
    if not premisser:
        yield theta
        return
    p, rest = premisser[0], premisser[1:]
    for f in sorted(kjente):
        if f[0] != p[0]:
            continue
        ny = dict(theta)
        if all(ny.setdefault(a, b) == b if a.islower() else a == b for a, b in zip(p[1:], f[1:])):
            yield from match(rest, ny, kjente)

totalt = 0
for k in range(1, maks_iterasjoner + 1):
    nye = set()
    for premisser, (pred, *args) in regler:
        for theta in match(premisser, {}, fakta):
            q = (pred, *[theta.get(a, a) for a in args])
            if q not in fakta:
                nye.add(q)
    if not nye:
        print(f"Iterasjon {k}: ingen nye fakta, fikspunktet er nådd")
        break
    fakta |= nye
    totalt += len(nye)
    print(f"Iterasjon {k}: " + ", ".join(f"{p}({a}, {b})" for p, a, b in sorted(nye)))
print(f"Nye fakta totalt: {totalt}")

Fremoverkjeding passer når fakta strømmer inn og du vil ha alle konsekvensene, for eksempel i et system som oppdaterer hvem som har nøkkel hver gang noen betaler. Bakoverkjeding passer når du har ett spørsmål og en stor KB, fordi den bare rører reglene som kan bidra til svaret.

Bakoverkjeding starter i spørringen, som i utsagnslogikk, men hvert mål kan inneholde variabler, og bindingene følger med nedover i treet. Er spørringen $\text{Invitert}(w)$, er svaret bindingen $w$ har fått når alle delmålene er bevist. Søket går dybde først med premissene fra venstre. Det bruker lite minne, men kan gjenta delmål og gå i løkke på rekursive regler som $\text{Naar}(x,y)\wedge \text{Naar}(y,z)\Rightarrow \text{Naar}(x,z)$, der første delmål har samme form som målet. Løkkesjekk og lagring av delresultater hjelper.

I bevistreet under er R2 skrevet med variabelen $z$, så den ikke kolliderer med $y$ i R1. Bindingen $y/\text{Siri}$ fra første premiss følger med til andre premiss, som derfor blir målet $\text{Leder}(\text{Siri})$ og ikke $\text{Leder}(y)$.

Resolusjon i FOL trenger klausuler, som i utsagnslogikk, men nå med variabler og uten kvantorer. Konverteringen har seks navngitte steg:

1. 1.Fjern $\iff$ og $\Rightarrow$.
2. 2.Flytt $\neg$ innover, også forbi kvantorer: $\neg \forall xP$ blir $\exists x\neg P$, og $\neg \exists xP$ blir $\forall x\neg P$.
3. 3.Standardiser variablene, så hver kvantor har sin egen variabel.
4. 4.Skolemiser: fjern hver $\exists$.
5. 5.Dropp $\forall$. Alle variabler som står igjen, er universelt kvantifisert.
6. 6.Distribuer $\vee$ over $\wedge$.

Steg 4, Skolemisering (Skolemization), er det nye. En $\exists$ uten noen $\forall$ rundt seg blir en Skolem-konstant (Skolem constant): $\exists h\text{Hytte}(h)$ blir $\text{Hytte}(C_1)$, som ved EI. Står $\exists$ inne i én eller flere $\forall$, kan verdien avhenge av dem, og variabelen blir en Skolem-funksjon (Skolem function) av alle de omsluttende $\forall$-variablene. I $\forall x(\text{Medlem}(x)\Rightarrow \exists s\text{Eier}(x,s))$ kan hvert medlem ha sin egen tursekk, så $s$ blir $F_1(x)$, ikke én felles $C_1$. Med to omsluttende kvantorer får funksjonen to argumenter: i $\forall x\forall t\exists y\text{Fulgte}(y,x,t)$ blir $y$ til $F_1(x,t)$.

Standardiseringen i steg 3 trengs når samme variabel er bundet av to kvantorer. I $(\forall x\text{Medlem}(x))\vee (\exists x\text{Leder}(x))$ er de to $x$-ene uavhengige, og den andre får et nytt navn, $x_1$, før kvantorene fjernes. Ellers ville skolemiseringen og dropp-steget blandet dem sammen.

To ting avgjør om en $\exists$ skolemiseres, og til hva. Negasjonene må være flyttet inn først, og bare kvantorene som omslutter $\exists$, teller. En $\exists$ i premisset til en implikasjon blir $\forall$ i steg 2 og skal ikke skolemiseres, så lenge implikasjonen ikke selv står under en negasjon. I et negert mål kan den samme $\exists$-en bli stående og må skolemiseres. Det sikre er alltid å flytte $\neg$ helt inn først.

Den første påstanden under gjelder hvert medlem, den andre er en negert $\forall$.

Førsteordens resolusjon er utsagnslogisk resolusjon med unifisering (ƒbinær resolusjon med unifikator). To klausuler resolveres når en literal i den ene unifiserer med negasjonen av en literal i den andre, og θ brukes på hele resolventen:

Her er $\theta =\{x/w,y/\text{Ivar}\}$.

Klausulene standardiseres fra hverandre før hvert steg. Skriv hvert steg som én linje med begge foreldrene, θ og resolventen, slik at den som leser, kan sjekke at θ gjør literalene komplementære og at θ er brukt på alt som står igjen. To literaler i samme klausul som unifiserer, slås sammen ved faktorisering (factoring), og binær resolusjon sammen med faktorisering er fullstendig for motsigelser.

Faktorisering trengs fordi binær resolusjon bare fjerner én literal fra hver forelder. Fra $P(x)\vee P(y)$ og $\neg P(u)\vee \neg P(v)$ gir hvert binære steg en ny klausul med to literaler, så □ kommer aldri. Faktoriser først, til $P(x)$ og $\neg P(u)$, og ett steg gir □.

Bevis ved motsigelse virker som før: legg det negerte målet til KB, gjør alt om til klausuler og resolver til □. Pass på det negerte målet (ƒdet negerte ∀-målet). Målet $\exists w\text{Besteforelder}(w,\text{Siv})$ negert er $\forall w\neg \text{Besteforelder}(w,\text{Siv})$, altså klausulen $\neg \text{Besteforelder}(w,\text{Siv})$ med en variabel. Målet $\forall x(A(x)\Rightarrow B(x))$ negert er $\exists x(A(x)\wedge \neg B(x))$, som gir Skolem-konstanten i $A(C_1)$ og $\neg B(C_1)$.

Når målet har en variabel, gir beviset også et svar. Bindingen variabelen får gjennom beviset, er den som gjør målet sant; det kalles svarekstraksjon (answer extraction). Svaret kan også være en Skolem-term. Lærer beviset bare at «medlemmet som lånte atlaset» har lånekort, blir bindingen noe som $F_1(\text{Atlas})$: et objekt KB vet finnes, men ikke har navn på.

I slektstavlen under spør vi hvem som er besteforelder til Siv.