Begreper & referanser
Alle nøkkelbegrepene, formlene og referansene fra Utsagnslogikk: syntaks, semantikk og entailment, 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.
En mengde setninger i et formelt språk som beskriver det en agent vet om verden. Forkortes KB, og leses som konjunksjonen av setningene (knowledge base).
De to operasjonene mot en kunnskapsbase: TELL legger til en ny setning, og ASK spør om noe, der svaret må følge av det som er fortalt (TELL / ASK).
Reglene for hvilke setninger som er velformet i et språk, for eksempel at er en setning og ikke er det (syntax).
Reglene for når en setning er sann. I utsagnslogikk gir semantikken sannhetsverdien til en setning i hver modell, ett konnektiv om gangen (semantics).
Et enkelt utsagnssymbol som eller , eller en av konstantene og . Alle andre setninger bygges av atomære setninger med konnektiver (atomic sentence).
Et symbol som lager en ny setning av én eller to setninger: , , , og . Uten parenteser binder de i den rekkefølgen (logical connective).
En tilordning av sann eller usann til hvert utsagnssymbol. Med symboler finnes modeller, én per rad i sannhetstabellen (model).
er en logisk konsekvens av KB, , når er sann i hver modell der KB er sann (entailment).
Å avgjøre ved å gå gjennom alle modellene og sjekke i hver modell der KB er sann. Sunn og fullstendig, men tiden er (model checking).
En inferensalgoritme er sunn når den bare utleder setninger som er logiske konsekvenser av KB. Den finner aldri på noe (sound inference).
En inferensalgoritme er fullstendig når den kan utlede hver setning som er en logisk konsekvens av KB (complete inference).
En setning som er sann i alle modeller, også kalt tautologi, for eksempel (valid sentence).
En setning som er sann i minst én modell. En setning som ikke er oppfyllbar, er uoppfyllbar, og da er negasjonen gyldig (satisfiable sentence).
To setninger er logisk ekvivalente, , når de er sanne i nøyaktig de samme modellene (logical equivalence).
hvis og bare hvis implikasjonen er gyldig (deduction theorem).
Å vise ved å vise at er uoppfyllbar: antar du det motsatte av konklusjonen, finnes ingen modell (proof by refutation).
Formler
Hver formel: hva den heter, hvordan den ser ut, og hva symbolene betyr.
Logisk konsekvens som delmengde
Grunnlaget for modellsjekking: alle modellene til må også være modeller av . Vanlig feil er å sjekke radene der er sann, i stedet for radene der er sann.
Deduksjonsteoremet
Gjør et spørsmål om logisk konsekvens til et spørsmål om gyldighet. står mellom setninger, inne i en setning; de er ikke det samme symbolet.
Bevis ved motsigelse
Brukes av resolusjon i kapittel 12: legg til negasjonen av målet og vis at det ikke finnes noen modell. Vanlig feil er å negere hele KB i stedet for målet.
Implikasjonseliminasjon
Viser at en implikasjon bare er usann når premisset er sant og konklusjonen usann. Brukes i hver CNF-omforming.
Logisk ekvivalens
To setninger er ekvivalente når hver følger av den andre, altså når de har de samme modellene. Kontraposisjonen er et eksempel; er det ikke.
Antall modeller
Med utsagnssymboler har sannhetstabellen rader. Hvert nytt symbol dobler arbeidet for modellsjekking.
Kodesnutter
Kodesnutter fra kapittelet, vist literal.
Modellsjekking av en liten kunnskapsbase
import itertools n_symboler = 3 # @param 3..14vindu_aapent = 1 # @param 0..1 # F: fuktig på badet, L: vifta går, V: vinduet er åpent, X: ekstra symbolersymboler = ["F", "L", "V"] + [f"X{i}" for i in range(1, n_symboler - 2)]kb = [ lambda m: not m["F"] or m["L"] or m["V"], # F ⇒ L ∨ V lambda m: not m["V"] or not m["L"], # V ⇒ ¬L lambda m: m["F"], # F lambda m: m["V"] == bool(vindu_aapent), # V eller ¬V]alfa = lambda m: not m["L"] # α = ¬L sjekket = sanne = 0moteksempel = Nonefor verdier in itertools.product([True, False], repeat=n_symboler): m = dict(zip(symboler, verdier)) sjekket += 1 if all(f(m) for f in kb): sanne += 1 if not alfa(m) and moteksempel is None: moteksempel = m print(f"Modeller sjekket: {sjekket}")print(f"Modeller der KB er sann: {sanne}")print(f"KB ⊨ α: {'nei' if moteksempel else 'ja'}")if moteksempel: tekst = ", ".join(f"{s} = {int(moteksempel[s])}" for s in "FLV") print(f"Moteksempel: {tekst}")else: print("Moteksempel: ingen")Prøv: sett vindu_aapent til 0 og se at linja KB ⊨ α: blir nei og Moteksempel: viser modellen der vifta går, og øk så n_symboler og se Modeller sjekket: doble seg for hvert symbol.
Læringsmål
Hva du skal kunne etter å ha lest kapittelet.
- 01Forklar hvordan en kunnskapsbasert agent bruker TELL og ASK, og skill syntaks fra semantikk
- 02Les setninger med riktig presedens, og regn ut sannhetsverdien i hver modell med en sannhetstabell
- 03Avgjør om ved modellsjekking, og pek ut et moteksempel når den ikke følger
- 04Klassifiser setninger som gyldige, oppfyllbare eller uoppfyllbare, og begrunn med en modell eller et moteksempel
- 05Bruk deduksjonsteoremet og bevis ved motsigelse til å omforme et spørsmål om logisk konsekvens
- 06Formaliser norske setninger med «bare hvis», «med mindre» og «verken … eller» i utsagnslogikk