English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/134120
Share/Impact:
Statistics
logo share SHARE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL
Exportar a otros formatos:

Title

On the implementation of a Fuzzy DL Solver over Infinite-Valued Product Logic with SMT Solvers

AuthorsAlsinet, Teresa; Barroso, David; Bejar, Ramon; Bou, Felix; Cerami, Marco; Esteva, Francesc
KeywordsDescription logics
Fuzzy product logic
SMT solvers
Issue Date2013
PublisherSpringer
CitationLecture Notes in Artificial Intelligence 8078. Scalable Uncertainty Management, 7th International Conference, SUM 2013 Washington, DC, USA, September 16-18, 2013, Proceedings, pp 325-330.
AbstractIn 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 SMT solver. 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.
URIhttp://hdl.handle.net/10261/134120
DOI10.1007/978-3-642-40381-1_25
Identifiersdoi: 10.1007/978-3-642-40381-1_25
issn: 0302-9743
isbn: 978-3-642-40380-4
Appears in Collections:(IIIA) Libros y partes de libros
Files in This Item:
File Description SizeFormat 
LNCS8078_p.325-30.pdf160,92 kBUnknownView/Open
Show full item record
Review this work
 


WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.