17.01.2008

O łączeniu programów w logice i teorii pierwszego rzędu

Dla zastosowań związanych z "Semantic Web" duże znaczenie mają tzw. ontologie. Można je traktować jako logiki deskryptywne (description logics) - ograniczone podklasy logiki pierwszego rzędu wyposażone w wydajne systemy wnioskowania. Innym ważnym narzędziem są systemy reguł. Można je traktować jako programy w logice (logic programs). Często formułowana jest potrzeba łączenia obydwu formalizmów. Główną ich różnicą jest to, że programy w logice są niemonotoniczne - dodanie aksjomatu do teorii może spowodować, że pewne konsekwencje teorii przestaną obowiązywać.
Przedstawię reguły hybrydowe - sposób łączenia programów w logice z negacją (normal logic programs) z dowolnymi teoriami pierwszego rzędu. Semantyka reguł hybrydowych jest połączeniem semantyki dobrze ufundowanej (well-founded semantics) programów w logice, oraz standardowej semantyki logiki pierwszego rzędu. Przedstawię również semantykę operacyjną, czyli sposób obliczania konsekwencji dla zbiorów reguł hybrydowych.
Istniejące podejścia do łączenia reguł i logik deskryptywnych wychodzą z semantyki modeli stabilnych (stable models, lub answer sets), a nie semantyki dobrze ufundowanej. W porównaniu z nimi nasze podejście ma efektywniejszą semantykę operacyjną i/lub bardziej elegancką semantykę logiczną.
Współautorem jest Jan Małuszyński (Szwecja). Jakob Henriksson (Niemcy) jest współautorem prototypowej implementacji