Resolution Based Reasoning in Description Logic

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61988987%3A17610%2F06%3A00000008" target="_blank" >RIV/61988987:17610/06:00000008 - isvavai.cz</a>

Alternative codes found

RIV/61988987:17310/06:00000013

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Resolution Based Reasoning in Description Logic

Original language description

The article presents refutational resolution theorem proving system for Description Logic (DL) based on general (non-clausal) resolution rule. There is also presented unification algorithm handling existentiality without the need of skolemization in first-order logic. Its idea follows from general resolution with existentiality for first-order logic. With this system existing resolution strategies may be used.

Czech name

Resolution Based Reasoning in Description Logic

Czech description

The article presents refutational resolution theorem proving system for Description Logic (DL) based on general (non-clausal) resolution rule. There is also presented unification algorithm handling existentiality without the need of skolemization in first-order logic. Its idea follows from general resolution with existentiality for first-order logic. With this system existing resolution strategies may be used.

Type

A - Audiovisual production

CEP classification

JD - Use of computers, robotics and its application

OECD FORD branch

—

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2006

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

ISBN

80-248-1001-8

Place of publication

Hradec Králové

Publisher/client name

FIM UHK

Version

Přednáška

Carrier ID

—