Joanna Golińska-Pilarek (UW)
Automatyzacja wnioskowań z wykorzystaniem relacyjnych systemów dual tableau

Logiczna reprezentacja wiedzy jest jednym z kluczowych problemów sztucznej inteligencji. Ostatnie dziesięciolecia pokazały, że metody logiczne znajdują nieoczekiwane zastosowania w rozmaitych dziedzinach wiedzy, w szczególności w kognitywistyce, lingwistyce, czy technologiach informacyjnych.

Relacyjne systemy dedukcyjne w stylu dual tableaux (dualne systemy tablicowe) stanowią ważny nurt badań w teorii automatycznej dedukcji i logicznej reprezentacji wiedzy. Systemy te są dobrym narzędziem realizacji trzech głównych zadań logicznych, leżących u podstaw wszystkich związanych z IT metod formalnych: weryfikacji prawdziwości (validity checking), weryfikacji spełniania (model checking), weryfikacji wynikania (entailment).

Dualne systemy tablicowe oparte są na diagramach Rasiowej-Sikorskiego dla klasycznej logiki pierwszego rzędu [RAS60]. Zakres ich stosowalności jest bardzo szeroki, w szczególności systemy takie skonstruowano dla wielu teorii badanych tradycyjnie przez matematyków i filozofów (logiki klasyczne, modalne, intuicjonistyczne, wielowartościowe), teorii mających swoje źródło w systemach informacyjnych (logiki dla wnioskowań przy niepełnej, przybliżonej i rozmytej informacji), jak i innych teorii znajdujących zastosowania w AI.

Logika relacyjna umożliwia konstrukcję dualnych systemów tablicowych w sposób systematyczny i modularny. Logika ta, wprowadzona w pracach Profesor Ewy Orłowskiej ([ORŁ88], [ORŁ97]), jest świetnym narzędziem umożliwiającym reprezentację w ramach jednego formalizmu trzech najważniejszych składowych systemu logicznego: syntaktyki, semantyki i dedukcji. Okazało się, że system dla klasycznej logiki relacyjnej jest wspólnym jądrem większości dualnych systemów tablicowych. To zaś oznacza, że w przypadku nowej teorii mającej relacyjną reprezentację nie musimy budować jej systemu dedukcyjnego od początku; wystarczy rozszerzyć bazowy system o reguły odpowiadające tym własnościom, które dla danej teorii są specyficzne.

Dualne systemy tablicowe stanowią alternatywę dla innych metod dedukcyjnych takich, jak systemy tablicowe, rachunek sekwentów Genztena, rezolucja czy systemy Hilbertowskie. Pełny opis możliwości zastosowań relacyjnych systemów dedukcyjnych zawiera monografia [ORG11].

W trakcie referatu omówię ogólną metodologię tworzenia systemów typu dual tableaux, przedstawię kilka przykładów takich systemów i przedyskutuję zagadnienia związane z ich implementacją i efektywnością obliczeniową.

Prezentacja (przedstawiona na Konferencji)

LITERATURA

[ORŁ88] E. Orłowska. Relational interpretation of modal logics, w: H. Andreka, D. Monk, I. Nemeti (eds.), Algebraic Logic. Colloquia Mathematica Societatis Janos Bolyai 54, North Holland, Amsterdam, 443–471 (1988).

[ORŁ97] E. Orłowska. Relational semantics for non-classical logics: Formulas are relations, w: J. Wolenski (ed.), Philosophical Logic in Poland, Kluwer, 167–186 (1994).

[ORG11] E. Orłowska, J. Golińska-Pilarek. Dual Tableaux: Foundations, Methodology, Case Studies, Trends in Logic 36, Springer Science, 2011.

[RAS60] H. Rasiowa, R. Sikorski. On Gentzen theorem, Fundamenta Mathematicae 48, 57–69 (1960).

Dodaj komentarz

Twój adres email nie zostanie opublikowany. Pola, których wypełnienie jest wymagane, są oznaczone symbolem *