Non-clausal Resolution Theorem Proving for Fuzzy Description Logic
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61988987%3A17610%2F06%3A00000006" target="_blank" >RIV/61988987:17610/06:00000006 - isvavai.cz</a>
Nalezeny alternativní kódy
RIV/61988987:17310/06:00000011
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Non-clausal Resolution Theorem Proving for Fuzzy Description Logic
Popis výsledku v původním jazyce
The article presents refutational resolution theorem proving system for the Fuzzy Description Logic based on the general (non-clausal) resolution rule. There is also presented a unification algorithm handling existentiality without the need of skolemization. This formalism integrates previously created provers for classical description logic and for fuzzy predicate logic. The problem of automated reasoning concerning fuzzy logic requires more complex methods in contrast to classical logic. Presented formalism overcomes the key unsolvable obstacle - clausal normal form generation (in fuzzy logic) - by introduction of generally applicable inference rule (working with general formulas not only clauses).
Název v anglickém jazyce
Non-clausal Resolution Theorem Proving for Fuzzy Description Logic
Popis výsledku anglicky
The article presents refutational resolution theorem proving system for the Fuzzy Description Logic based on the general (non-clausal) resolution rule. There is also presented a unification algorithm handling existentiality without the need of skolemization. This formalism integrates previously created provers for classical description logic and for fuzzy predicate logic. The problem of automated reasoning concerning fuzzy logic requires more complex methods in contrast to classical logic. Presented formalism overcomes the key unsolvable obstacle - clausal normal form generation (in fuzzy logic) - by introduction of generally applicable inference rule (working with general formulas not only clauses).
Klasifikace
Druh
A - Audiovizuální tvorba
CEP obor
JD - Využití počítačů, robotika a její aplikace
OECD FORD obor
—
Návaznosti výsledku
Projekt
—
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
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ů
Údaje specifické pro druh výsledku
ISBN
80-903298-4-5
Místo vydání
Praha
Název nakladatele resp. objednatele
Institute of Computer Science, Czech Academy of Sciences
Verze
Přednáška
Identifikační číslo nosiče
—