Exploiting SAT Technology for Axiom Pinpointing

Norbert MantheyNorbert Manthey, Rafael PeñalozaRafael Peñaloza

Download

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

Details
Bibtex

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:Further Information: Link
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory, WissensverarbeitungKnowledge Representation and Reasoning

@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}
}