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 \(\mathcal{FL}_0\). The new algorithm has only worst-case exponential runtime, in contrast to the previous one which was even best-case exponential.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F., Narendran, P.: Unification of concept terms in description logics. J. Symb. Comput. 31(3), 277–305 (2001)
Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Appl. Log. 7(1), 58–74 (2009)
Birget, J.: State-complexity of finite-state devices, state compressibility and incompressibility. Math. Syst. Theory 26(3), 237–269 (1993)
Borgwardt, S., Morawska, B.: Finding finite Herbrand models. LTCS-Report 11-04, TU Dresden (2011), http://lat.inf.tu-dresden.de/research/reports.html
Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)
Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007), http://www.grappa.univ-lille3.fr/tata
Dreben, B., Goldfarb, W.D.: The Decision Problem: Solvable Classes of Quantificational Formulas. Addison-Wesley (1979)
Joyner Jr., W.H.: Resolution strategies as decision procedures. J. ACM 23(3), 398–417 (1976)
Ladner, R.E., Lipton, R.J., Stockmeyer, L.J.: Alternating pushdown and stack automata. SIAM J. Comput. 13(1), 135–155 (1984)
Leitsch, A.: The Resolution Calculus. Springer, Heidelberg (1997)
Peltier, N.: Model building with ordered resolution: Extracting models from saturated clause sets. J. Symb. Comput. 36(1-2), 5–48 (2003)
Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Uni Bonn (1962)
Reisig, W.: Petri Nets: An Introduction. Springer, Heidelberg (1985)
Slutzki, G.: Alternating tree automata. Theor. Comput. Sci. 41, 305–318 (1985)
Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs (extended abstract). In: Proc. STOC 1984, pp. 446–456. ACM (1984)
Zhang, J.: Constructing finite algebras with FALCON. J. Autom. Reasoning 17, 1–22 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Borgwardt, S., Morawska, B. (2012). Finding Finite Herbrand Models. In: Bjørner, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2012. Lecture Notes in Computer Science, vol 7180. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28717-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-28717-6_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28716-9
Online ISBN: 978-3-642-28717-6
eBook Packages: Computer ScienceComputer Science (R0)