Finding Finite Herbrand Models

Stefan BorgwardtStefan Borgwardt, Barbara MorawskaBarbara Morawska

Download

Stefan Borgwardt, Barbara Morawska
Finding Finite Herbrand Models
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, volume 11-04, 2011. LTCS-Report

Details
Bibtex

KurzfassungAbstract
We show that finding finite Herbrand models for a restricted class of first-order clauses is ExpTime-complete. A Herbrand model is called finite if it interprets all predicates by finite subsets of the Herbrand universe. The restricted class of clauses consists of anti-Horn clauses with monadic predicates and terms constructed over unary function symbols and constants. The decision procedure can be used as a new goal-oriented algorithm to solve linear language equations and unification problems in the description logic FL_0. The new algorithm has only worst-case exponential runtime, in contrast to the previous one which was even best-case exponential.
Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ BoMo-LTCS-11-04,
  address = {Dresden, Germany},
  author = {Stefan {Borgwardt} and Barbara {Morawska}},
  institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
  note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
  number = {11-04},
  title = {Finding Finite {H}erbrand Models},
  type = {LTCS-Report},
  year = {2011},
}