Finding Finite {H}erbrand Models

Stefan BorgwardtStefan Borgwardt, Barbara MorawskaBarbara Morawska

Download

Stefan Borgwardt, Barbara Morawska
Finding Finite {H}erbrand 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},
}