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

Publication Type | Conference Paper |

Year of Publication | 2013 |

Authors | Alsinet T [1], Barroso D [2], Bejar R [3], Bou F [4], Cerami M [5], Esteva F [6] |

Conference Name | 7th International Conference on Scalable Uncertainty Management, SUM 2013 |

Volume | 8078 |

Edition | Weiru Liu, V. S. Subrahmanian and Jef Wijsen |

Publisher | Springer |

Pagination | 325-330 |

Date Published | 16/09/2013 |

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

URL | http://link.springer.com/chapter/10.1007%2F978-3-642-40381-1_25 [7] |