Ontológia alapú tudásreprezentáció és bizonyítás

OData támogatás
Konzulens:
Dr. Pataricza András
Méréstechnika és Információs Rendszerek Tanszék

A tudásszerzési folyamat célja olyan, egy adott alkalmazási körben általános érvényű ismeretrendszer feltárása, amely újraalkalmazva támogatja a hasonló körben történő eligazodást. Ezutóbbi tudásalkalmazási fázis előfeltétele annak eldönthetősége, hogy az ismerethalmaz mely részei alkalmazhatóak; és amennyiben az alkalmazhatóság fennáll, akkor a korábban megszerzett ismereteket az új környezetbe beépítsük.

Ahhoz, hogy ezt hatékonyan meg tudjuk tenni, megfelelő tudásreprezentációra van szükség.

A tudásreprezentációval szemben alapvető igény az elsődleges tudásforrásból származó, újrafelhasználásra szánt ismeretek helyességének és teljességének ellenőrizhetősége. Az újrafelhasználás során ugyanis akár téves információ beépítése, akár pedig egy szituáció következményének hiányos felmérése koncepcionális hibát okozhat. A fenti kérdések matematikai szabatosságú vizsgálata formalizált tudásreprezentációt igényel.

Tudásreprezentáció céljára széles körben ontológiákat használnak. A helyesség bizonyításának alapvető, a reprezentált tudástól független módja a felépített ontológia konzisztenciájának és teljességének vizsgálata. Kiegészítő lehetőség néhány, az adott ismeretkörnyezetben előzetesen ismert igazságtartalmú állítás és az ontológia konzisztenciájának vizsgálata, kizárólag a modellben szereplő információra támaszkodva. Az ilyen logikai ellenőrzést ma tipikusan az úgynevezett következtetőgépek (reasoner-ek) végzik.

Az ezek által vizsgálható kérdések sajnos nem minden esetben fedik le a mérnöki alkalmazások által támasztott követelményeket, elsősorban a feltehető kérdések bonyolultságának korlátos volta miatt.

Az ontológiák leképezhetők a ma legbonyolultabb műszaki problémák megválaszolására széleskörűen használt kielégíthetőségi problémát (SAT) vizsgáló eszközök bemenő modelljére.

A szakdolgozat azt vizsgálja, hogy SAT-megoldók segítségével milyen jellegű és nehézségű következtetéseket lehet tenni egy ontológia felett. Leírja az ontológia-SAT leképezést és ismerteti annak egy implementációját, amely a Protégé ontológiaépítő környezetet illeszti a Z3 SAT-megoldóhoz.

Ezzel a módszerrel összetettebb bizonyításokat lehet végezni, mint a jelenlegi eszközökkel. Megfelelő használatával támogatható az ontológiaépítés valamint karbantartás is. A Z3 megoldó képességeit kihasználva új módszer adódik az inkonzisztenciák felderítésére is.

Letölthető fájlok

A témához tartozó fájlokat csak bejelentkezett felhasználók tölthetik le.