Begreper & referanser
Alle nøkkelbegrepene, formlene og referansene fra Inferens i førsteordens logikk, 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.
Inferensregelen som fra gir med byttet ut med en grunnterm. Den kan brukes så mange ganger du vil, med ulike termer (Universal Instantiation, UI).
Inferensregelen som fra gir med byttet ut med en ny konstant som ikke finnes i KB. Den brukes én gang, og etterpå kan -setningen fjernes (Existential Instantiation, EI).
Å gjøre en førsteordens KB om til utsagnslogikk ved å instansiere hver universell setning med alle grunntermer og hver eksistensiell setning med en ny konstant (propositionalization).
En mengde bindinger, som , som bytter variabler med termer. er med bindingene brukt (substitution).
Å finne en substitusjon som gjør to atomer eller termer like, eller å avgjøre at ingen finnes (unification).
Unifikatoren som binder minst mulig: alle andre unifikatorer får du ved å binde videre. Den er entydig opp til navn på variabler (most general unifier, MGU).
Sjekken i unifiseringen som nekter å binde en variabel til en term der variabelen selv står, som . Uten den kan unifiseringen lage en uendelig term (occurs check).
Å gi variablene i hver klausul eller regel egne navn før unifisering, så to setninger aldri deler en variabel ved et uhell (standardizing apart).
Inferensregelen som fra fakta og regelen gir , der én θ gjør hvert likt (Generalized Modus Ponens, GMP).
Å gjøre en utsagnslogisk inferensregel om til en førsteordens regel med variabler ved hjelp av unifisering. Generalisert modus ponens er løftet modus ponens (lifting).
Førsteordens definitte klausuler uten funksjonssymboler. Det finnes bare endelig mange grunne atomer, så fremoverkjeding stopper alltid (Datalog).
Å fjerne ved å bytte den bundne variabelen med en ny konstant, eller med en ny funksjon av de omsluttende -variablene. Resultatet er oppfyllbart nøyaktig når originalen er det (Skolemization).
Den nye konstanten skolemiseringen bruker når ingen omslutter , skrevet , og så videre (Skolem constant).
Den nye funksjonen skolemiseringen bruker når står inne i én eller flere , med de omsluttende variablene som argumenter, som eller (Skolem function).
Å slå sammen to literaler i samme klausul som kan unifiseres, for eksempel til . Binær resolusjon sammen med faktorisering er fullstendig for motsigelser (factoring).
Å lese svaret på et «hvem»-spørsmål av bindingene i et resolusjonsbevis: bindingen variabelen i det negerte målet får, er svaret (answer extraction).
To strategier for å velge resolusjonssteg. Støttemengde krever at hvert steg bruker det negerte målet eller en klausul avledet fra det, og enhetspreferanse resolverer helst med enhetsklausuler (set of support, unit preference).
Å bruke en likhet som til å bytte ut en term med den like termen i en annen klausul. Det er en måte å behandle likhet på i resolusjon (demodulation).
Formler
Hver formel: hva den heter, hvordan den ser ut, og hva symbolene betyr.
Regelen for universell instansiering
Gjelder for hver grunnterm , så du kan bruke den mange ganger med ulike termer. Brukes når en førsteordens KB gjøres om til utsagnslogikk.
Regelen for eksistensiell instansiering
Konstanten må være ny, ikke et navn som allerede finnes i KB. Regelen brukes én gang. I CNF gjør skolemiseringen samme jobb.
Definisjonen av UNIFY
Unifisering finner en θ som gjør to uttrykk like. Vi vil ha den mest generelle, og occurs check hindrer bindinger som .
Regelen for generalisert modus ponens
Én θ må passe alle premissene samtidig. Standardiser variablene i faktaene og regelen fra hverandre først, og vis både UNIFY og SUBST når du bruker regelen.
Det negerte ∀-målet
Når målet er en -setning, blir det negerte målet en -setning, og skolemiseringen gir en Skolem-konstant. Vanlig feil: å skrive og med en variabel, som sier noe helt annet.
Binær resolusjon med unifikator
Klausulene standardiseres fra hverandre først. Bruk θ på hele resolventen, ikke bare på literalene som forsvinner, og skriv θ på hver linje i beviset.
Kodesnutter
Kodesnutter fra kapittelet, vist literal.
Unifisering med og uten occurs check
occurs_check = 1 # @param 0..1 # Variabler er små bokstaver; ("Far", "y") er termen Far(y).a, b = ("Sammen", "x", ("LederAv", "x")), ("Sammen", ("Far", "y"), "y")er_var = lambda t: isinstance(t, str) and t[0].islower() def finn(t, th): # følg bindingene til en ubundet variabel eller en sammensatt term while er_var(t) and t in th: t = th[t] return t def forekommer(v, t, th): t = finn(t, th) return t == v or (isinstance(t, tuple) and any(forekommer(v, s, th) for s in t[1:])) def unify(s, t, th): if th is None: return None s, t = finn(s, th), finn(t, th) if s == t: return th if er_var(s) or er_var(t): v, u = (s, t) if er_var(s) else (t, s) return None if occurs_check and forekommer(v, u, th) else {**th, v: u} if not (isinstance(s, tuple) and isinstance(t, tuple) and s[0] == t[0] and len(s) == len(t)): return None for x, y in zip(s[1:], t[1:]): th = unify(x, y, th) return th def vis(t, th, d=0): # SUBST(θ, t), men stopp etter fire nivåer t = finn(t, th) if d < 4 else t if isinstance(t, str): return "…" if d >= 4 and er_var(t) else t return f"{t[0]}({', '.join(vis(s, th, d + 1) for s in t[1:])})" th = unify(a, b, {})print(f"Unifiserbar: {'ja' if th is not None else 'nei'}")tekst = "{" + ", ".join(f"{v}/{vis(u, {})}" for v, u in th.items()) + "}" if th is not None else "ingen, occurs check stopper bindingen"print(f"MGU: {tekst}" if occurs_check else f"θ uten occurs check (ikke gyldig): {tekst}")print(f"SUBST(θ, x): {vis('x', th) if th is not None else 'ingen θ'}")Prøv: sett occurs_check til 0 og se at Unifiserbar: blir ja, mens SUBST(θ, x): viser en term som aldri tar slutt.
Fremoverkjeding i Datalog, iterasjon for 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 = 0for 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}")Prøv: øk maks_iterasjoner fra 1 til 5 og se at hver ny linje Iterasjon har ett faktum mindre enn den forrige, til Nye fakta totalt: stopper på 10 ved fikspunktet.
Læringsmål
Hva du skal kunne etter å ha lest kapittelet.
- 01Bruk universell og eksistensiell instansiering, og forklar hvorfor logisk konsekvens i FOL bare er semi-avgjørbar
- 02Finn den mest generelle unifikatoren for to atomer i komponert form, med occurs check
- 03Bruk generalisert modus ponens med standardiserte variabler, og vis UNIFY og SUBST eksplisitt
- 04Spor fremoverkjeding i Datalog iterasjon for iterasjon, og forklar hvorfor bakoverkjeding kan gå i løkke
- 05Konverter en førsteordens formel til CNF med de seks navngitte stegene, med Skolem-konstanter og Skolem-funksjoner
- 06Bevis et mål med resolusjon ved motsigelse, med θ på hver linje, ned til □, og les svaret av bindingene