Abstract
Tradisjonelt brukes relasjonsmodellen som teoretisk rammeverk for
studier av databaser. Et alternativ er å modellere databasene i
1. ordens logikk, og i en slik modell kan man se på fakta som aksiomer
(``antatte sannheter''), mens søk etter fakta i databasen blir et
bevissøk. Relasjonsmodellen kan representeres som en 1.ordens teori ,
men førsteordens logikk har større uttrykkskraft enn
relasjonsmodellen, og man kan derfor gå lenger og tillate mer
komplekse formler i databasen. Dermed kan man også lage mer komplekse
databaser. Eksempler på dette er databaser som kan inneholde
slutningsregler sammen med fakta, databaser som kan inneholde
ufullstendig informasjon eller databaser som inneholder negativ
informasjon. Slike databaser kaller vi for deduktive databaser. Man
kan skille mellom ulike klasser av deduktive databaser etter hvilke
egenskaper de har.
Det vil også være naturlig å ta steget videre, og se på hvordan andre
logikker med alternative egenskaper egner seg som spørrespråk for en
database. I oppgaven har jeg tatt utgangspunkt i logikken Æ, som er en
utsagnslogisk modallogikk i ``only knowing'' - familien introdusert av
Levesque, . Æ har mulighet for å uttrykke defaulter direkte i språket.
Ved hjelp av en omskriving av en formel som representerer oppfatninger
kan man få et direkte uttrykk for modellene. Æ har dessuten en
naturlig utvidelse til flere agenter.
Oppgaven består av to deler. I den første delen ser jeg på hvordan et
språk for en deduktiv database kan representeres i Æ, disse kaller jeg
for Æ-databaser. Jeg ser på enkelte sentrale problemstillinger omkring
deduktive databaser, og ser på hvordan en Æ-database kan håndtere
disse problemene. I den andre delen av oppgaven har jeg sett hvordan
en teorembeviser for en beslektet logikk kan implementeres.
I motsetning til tradisjonelle deduktive databaser har jeg tatt
utgangspunkt i et enkelt språk for representasjon av fakta. Dette gjør
at man kan bygge en Æ-database med en relasjons-database i bunn, og et
fremtidig mål vil være å bygge en prototype på en slik database. Dette
kan gjøres ved å kombinere en relasjonsdatabase med en søkemotor
basert på teorembeviseren jeg har implementert. I oppgaven ser jeg på
en en utgave av Æ med bare en agent. For en slik database vil det være
tilstrekkelig med en SAT-teorembeviser, men for en
multiagent-utvidelse vil ikke dette være tilstrekkelig. For en
multi-agent utgave av en Æ-database vil teorembeviseren jeg beskriver
kunne brukes som utgangspunkt for en implementasjon.
Til slutt har jeg skissert noen anvendelser av systemet, spesielt
rettet mot semantisk web.