Finding Finite Herbrand Models

Stefan BorgwardtStefan Borgwardt, Barbara MorawskaBarbara Morawska

Download

Stefan Borgwardt, Barbara Morawska
Finding Finite Herbrand Models
In Nikolaj Bjørner and Andrei Voronkov, eds., Proceedings of the 18th International Conference on Logic for Programming, Artifical Intelligence, and Reasoning (LPAR'12), volume 7180 of Lecture Notes in Computer Science, 138-152, 2012. Springer

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 FL0. The new algorithm has only worst-case exponential runtime, in contrast to the previous one which was even best-case exponential.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ BoMo-LPAR-12,
  address = {M{\'e}rida, Venezuela},
  author = {Stefan {Borgwardt} and Barbara {Morawska}},
  booktitle = {Proceedings of the 18th International Conference on Logic for Programming, Artifical Intelligence, and Reasoning (LPAR'12)},
  editor = {Nikolaj {Bj{\o}rner} and Andrei {Voronkov}},
  pages = {138--152},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  title = {Finding Finite {H}erbrand Models},
  volume = {7180},
  year = {2012},
}