Inferens i første-ordens logikk 1 oppgave 6.12, 6.2, 6.7, 7.2, 7.5, T-1 (evn noen til slutt) (del ut NTNU-prosjekt til resten) vi skal nå ta for oss komplett resonnering med første-ordens logikk, slik at systemet vårt kan representere kunnskap i en kunnskapsbase, og svare på spørsmål eller bevise påstander på grunnlag av denne kunnskapsbasen - vi skal jobbe videre fra paragraf 6.4 - SUBST(theta, alpha) theta - binding list alpha - setning - tre nye inferens regler side 266 (innlysende, skriv opp kjapt): universell eliminasjon eksistensiell eliminasjon eksistensiell introduksjon - vi skal se på eksempelet øverst på side 267 (vis stensil) (sammenlikn verifiseringssystemer for banktjenester f.eks. AmEx) - generalisert modus ponens (skriv opp), eksempel hele side 269 - kanonisk form (Horn-setninger): P1 and P2 .... => Q (ikke alle setninger kan skrives på denne måten) - unification (forene, samle-prosedyre): se eksempel med knows, hates side 270, 271 - standardize apart, MGU 2 hvordan konstruere et resonneringsprogram? - forover-lenking: datadrevet ("enklere enn pseudo-koden") fyller ut premissene og trekker konklusjoner etterhvert kan generere mange irrelevante konklusjoner eks s 273, 274 - bakover-lenking ser på alle inmplikasjoner som har konklusjoner som forener (unify) med query, og ser så pa premissene til disse figur 9.3, 9.4 - stort sett: forover-lenking ved tillegg av ny kunnskap, bakover-lenking ved bevisførsel - modus ponens er inkomplett; derfor resolusjon: en komplett inferens prosedyre - prinsipielt de samme som for erklærende logikk, skriv opp nederst s 277 - disjunksjons og implikasjons resolusjons inferens regler: vis side 278, cluet er forening av p og q (unify) resolusjon er en generalisering av modus ponens - konjunktiv og impliserende normalform (vis side 279) vi bruker impliserende normal form, og skriver alfa, istedet for TRUE => alfa - lenking med resolusjon er heller ikke komplett, men bra nok - refutation er komplett (typisk matematisk), men brukes mest spesifikt for bevis (teorembevisprega) - konvertering til normal form: regler side 281, 282 merk Skolemize, Skolem funksjon - eksempel side 282 - heuristikker for resolusjonsstrategier, side 285 - oppgave 9.8 viktig til neste gang (ikke spesielt lang, i punkt c forklar skrittvis resolusjonen) 3