On the Implementation of a Fuzzy DL Solver over Infinite-Valued Product Logic with SMT Solvers
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989592%3A15310%2F13%3A33146836" target="_blank" >RIV/61989592:15310/13:33146836 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1007/978-3-642-40381-1_25" target="_blank" >http://dx.doi.org/10.1007/978-3-642-40381-1_25</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-40381-1_25" target="_blank" >10.1007/978-3-642-40381-1_25</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
On the Implementation of a Fuzzy DL Solver over Infinite-Valued Product Logic with SMT Solvers
Popis výsledku v původním jazyce
In this paper we explain the design and preliminary implementation of a solver for the positive satisfiability problem of concepts in a fuzzy description logic over the infinite-valued product logic. This very solver also answers 1-satisfiability in quasi-witnessed models. The solver works by first performing a direct reduction of the problem to a satisfiability problem of a quantifier free boolean formula with non-linear real arithmetic properties, and secondly solves the resulting formula with an SMTsolver. We show that the satisfiability problem for such formulas is still a very challenging problem for even the most advanced SMT solvers, and so it represents an interesting problem for the community working on the theory and practice of SMT solvers.
Název v anglickém jazyce
On the Implementation of a Fuzzy DL Solver over Infinite-Valued Product Logic with SMT Solvers
Popis výsledku anglicky
In this paper we explain the design and preliminary implementation of a solver for the positive satisfiability problem of concepts in a fuzzy description logic over the infinite-valued product logic. This very solver also answers 1-satisfiability in quasi-witnessed models. The solver works by first performing a direct reduction of the problem to a satisfiability problem of a quantifier free boolean formula with non-linear real arithmetic properties, and secondly solves the resulting formula with an SMTsolver. We show that the satisfiability problem for such formulas is still a very challenging problem for even the most advanced SMT solvers, and so it represents an interesting problem for the community working on the theory and practice of SMT solvers.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/EE2.3.30.0041" target="_blank" >EE2.3.30.0041: Podpora vytváření excelentních výzkumných týmů a intersektorální mobility na Univerzitě Palackého v Olomouci II.</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2013
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
Název statě ve sborníku
Scalable Uncertainty Management - 7th International Conference. Proceedings
ISBN
978-3-642-40380-4
ISSN
—
e-ISSN
—
Počet stran výsledku
6
Strana od-do
325-330
Název nakladatele
Springer
Místo vydání
Neuveden
Místo konání akce
Washington
Datum konání akce
16. 9. 2013
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—