Non-clausal Resolution Theorem Proving for Fuzzy Description Logic

Result code in 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>

Alternative codes found

RIV/61988987:17310/06:00000011

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Non-clausal Resolution Theorem Proving for Fuzzy Description Logic

Original language description

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).

Czech name

Non-clausal Resolution Theorem Proving for Fuzzy Description Logic

Czech description

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).

Type

A - Audiovisual production

CEP classification

JD - Use of computers, robotics and its application

OECD FORD branch

—

Project

—

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2006

Confidentiality

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

ISBN

80-903298-4-5

Place of publication

Praha

Publisher/client name

Institute of Computer Science, Czech Academy of Sciences

Version

Přednáška

Carrier ID

—