System automatycznej dedukcji dla logiki deskrypcyjnej z językiem ALCN

W artykule przedstawia się prosty system automatycznej dedukcji dla logiki deskrypcyjnej z językiem ALCN. Podstawową funkcją systemu jest badanie spełnialności pojęć oraz testowanie hipotez dotyczących relacji między pojęciami, tj. subsumpcji, równoważności i rozłączności. Do dedukcji wykorzystuje się metodę tabel analitycznych, a językiem implementacji systemu jest Prolog.

---

In this paper a simple automated deduction system for Description Logic with ALCN language is presented. It enables verification of four types of hypotheses concerning concepts, i.e. satisfiability, subsumption, equivalence and disjointness. The system uses an algorithm originating from semantic tableau calculus. The implementation has a form of relatively small program in Prolog language containing only elementary procedures, essential for soundness and completeness of inference process.