Abstract
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. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Borgwardt, S., & Morawska, B. (2012). Finding finite Herbrand models. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7180 LNCS, pp. 138–152). https://doi.org/10.1007/978-3-642-28717-6_13
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
