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%3A00000011" target="_blank" >RIV/61988987:17610/06:00000011 - isvavai.cz</a>
Alternative codes found
RIV/61988987:17310/06:00000014 RIV/61988987:17610/06:A1000DDP
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
Rezoluční dokazování v Deskripční logice
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.

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

Similar results(10)