Rezoluční dokazování v Deskripční logice

Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61988987%3A17610%2F06%3A00000011" target="_blank" >RIV/61988987:17610/06:00000011 - isvavai.cz</a>
Nalezeny alternativní kódy
RIV/61988987:17310/06:00000014 RIV/61988987:17610/06:A1000DDP
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.

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ů

Podobné výsledky(10)