Publ3 search

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.

Publikační činnost

Probíhá načítání, čekejte prosím...

Record type:	stať ve sborníku (D)
Home Department:	Ústav pro výzkum a aplikace fuzzy modelování (94410)
Title:	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.

Subtitle
Publication year:	2006
Obor:	Využití počítačů, robotika a její aplikace
Number of pages:	12
Page from:	106
Page to:	117
Form of publication:
ISBN code:	80-248-1001-8
ISSN code:
Proceedings title:	Proceedings of Znalosti 2006
Proceedings:
Publisher name:	FIM UHK
Place of publishing:	Hradec Králové
Country of Publication:	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ů:	Evropská akce
WoS code:
EID:

Key words in English:	Automated theorem proving, non-clausal resolution, general resolution, unification, description logic
Annotation in original language:	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.
Annotation in english language:	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.

References

Reference

R01:	RIV/61988987:17610/06:A1000DDP

Complementary Content

${loading}