Resolution Based Reasoning in Description Logic

Kód výsledku v 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>

Nalezeny alternativní kódy

RIV/61988987:17310/06:00000013

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Resolution Based Reasoning in Description Logic

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Resolution Based Reasoning in Description Logic

Popis výsledku anglicky

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.

Druh

A - Audiovizuální tvorba

CEP obor

JD - Využití počítačů, robotika a její aplikace

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2006

Kód důvěrnosti údajů

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

ISBN

80-248-1001-8

Místo vydání

Hradec Králové

Název nakladatele resp. objednatele

FIM UHK

Verze

Přednáška

Identifikační číslo nosiče

—