English   español  
Por favor, use este identificador para citar o enlazar a este item: http://hdl.handle.net/10261/134120
Compartir / Impacto:
Estadísticas
Add this article to your Mendeley library MendeleyBASE
Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL
Título

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

AutorAlsinet, Teresa; Barroso, David; Bejar, Ramon; Bou, Felix; Cerami, Marco; Esteva, Francesc
Palabras claveDescription logics
Fuzzy product logic
SMT solvers
Fecha de publicación2013
EditorSpringer
CitaciónLecture Notes in Artificial Intelligence 8078. Scalable Uncertainty Management, 7th International Conference, SUM 2013 Washington, DC, USA, September 16-18, 2013, Proceedings, pp 325-330.
ResumenIn 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
Identificadoresdoi: 10.1007/978-3-642-40381-1_25
issn: 0302-9743
isbn: 978-3-642-40380-4
Aparece en las colecciones: (IIIA) Libros y partes de libros
Ficheros en este ítem:
Fichero Descripción Tamaño Formato  
LNCS8078_p.325-30.pdf160,92 kBUnknownVisualizar/Abrir
Mostrar el registro completo
 


NOTA: Los ítems de Digital.CSIC están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.