Exploiting SAT Technology for Axiom Pinpointing

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche
Toggle side column

Exploiting SAT Technology for Axiom Pinpointing

Norbert MantheyNorbert Manthey,  Rafael PeñalozaRafael Peñaloza
Norbert Manthey, Rafael Peñaloza
Exploiting SAT Technology for Axiom Pinpointing
Technical Report, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, volume 15-05, 2015
  • KurzfassungAbstract
    Axiom pinpointing is the task of identifying the axioms that are responsible for a consequence.

    It is a fundamental step for tasks like ontology revision and context-based reasoning, among many others. One known approach is to reduce axiom pinpointing to an enumeration problem over a set of Horn clauses. We introduce the new SATPin system, which combines techniques from axiom pinpointing and minimal unsatisfiable subformula enumeration, and exploits the numerous optimizations developed for SAT solving in the last two decades. By adding a novel optimization method the runtime can improve by a factor up to 4300. Our experiments show that SATPin can find all the MinAs of large biomedical ontologies

    an order of magnitude faster than existing tools.
  • Weitere Informationen unter:Other info: Link
  • Forschungsgruppe:Research Group: AutomatentheorieWissensverarbeitung
@techreport{MP2015,
  author      = {Norbert Manthey and Rafael Pe{\~{n}}aloza},
  title       = {Exploiting {SAT} Technology for Axiom Pinpointing},
  institution = {Chair of Automata Theory, Institute of Theoretical Computer
                 Science, Technische Universit{\"{a}}t Dresden},
  year        = {2015}
}