OU Portal
Log In
Welcome
Applicants
Z6_60GI02O0O8IDC0QEJUJ26TJDI4
Error:
Javascript is disabled in this browser. This page requires Javascript. Modify your browser's settings to allow Javascript to execute. See your browser's documentation for specific instructions.
{}
Zavřít
Publikační činnost
Probíhá načítání, čekejte prosím...
publicationId :
tempRecordId :
actionDispatchIndex :
navigationBranch :
pageMode :
tabSelected :
isRivValid :
Typ záznamu
*
:
stať ve sborníku (D)
Domácí pracoviště
*
:
Ústav pro výzkum a aplikace fuzzy modelování (94410)
Název
*
:
Resolution Based Reasoning in Description Logic
Citace :
Habiballa, H. Resolution Based Reasoning in Description Logic.
In:
Proceedings of Znalosti 2006.
Hradec Králové: FIM UHK, 2006. FIM UHK, 2006. s. 106-117. ISBN 80-248-1001-8.
Podnázev :
Rok
*
:
2006
Obor
*
:
Využití počítačů, robotika a její aplikace
Počet stran
*
:
12
Strana od
*
:
106
Strana do
*
:
117
Forma vydání
*
:
Kód ISBN
*
:
80-248-1001-8
Kód ISSN :
Název sborníku
*
:
Proceedings of Znalosti 2006
Sborník :
Název nakladatele
*
:
FIM UHK
Místo vydání
*
:
Hradec Králové
Stát vydání :
Sborník vydaný v ČR
Název konference :
ZNALOSTI 2006
Místo konání konference
*
:
Hradec Králové
Datum zahájení konference
*
:
Typ akce podle státní
příslušnosti účastníků akce
*
:
Evropská akce
Kód UT WoS :
EID :
Klíčová slova anglicky
*
:
Automated theorem proving, non-clausal resolution, general resolution, unification, description logic
Popis 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.
Popis v anglické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.
Typ zdroje financování výsledku
*
:
Projekty CEP/Záměry CEZ
Seznam projektů :
ID Projektu
Název projektu
Seznam ohlasů :
Ohlas
R01:
RIV/61988987:17610/06:A1000DDP
Complementary Content
Deferred Modules
${title}
${badge}
${loading}
Deferred Modules