Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations

  • Bernhard Gramlich
  • Reinhard Pichler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)


Automated model building has evolved as an important sub-discipline of automated deduction over the past decade. One crucial issue in automated model building is the selection of an appropriate (finite) representation of (in general infinite) models. Quite a few such formalisms have been proposed in the literature. In this paper, we concentrate on the representation of Herbrand models by ground atoms with ground equations (GAE-models), introduced in [9]. For the actual work with any model representation, efficient algorithms for two decision problems are required, namely: The clause evaluation problem (i.e.: Given a clause C and a representation \( \mathcal{M} \) of a model, does C evaluate to “true” in this model?) and the model equivalence problem (i.e.: Given two representations \( \mathcal{M}_1 \) and \( \mathcal{M}_2 \), do they represent the same model?). Previously published algorithms for these two problems in case of GAE-models require exponential time. We prove that the clause evaluation problem is indeed intractable (that is, coNP-complete), whereas the model equivalence problem can be solved in polynomial time. Moreover, we show how our new algorithm for the model equivalence problem can be used to transform an arbitrary GAE-model into an equivalent one with better computational properties.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    F. Baader and T. Nipkow. Term rewriting and All That. Cambridge University Press, 1998.Google Scholar
  2. 2.
    P. Baumgartner, C. Fermüller, N. Peltier, and H. Zhang. Workshop: Model Computation-Principles, Algorithms, Applications. In D. McAllester, ed., Proc. 17th Int. Conf. on Automated Deduction (CADE’00), LNAI 1831, p. 513, Pittsburgh, PA, USA, June 2000. Springer-Verlag.Google Scholar
  3. 3.
    R. Caferra and N. Peltier. Extending semantic resolution via automated model building: Applications. In Proc. 14th Int. Conf. on Artificial Intelligence (IJ-CAI’95), pp. 328–334, Montréal, Québec, Canada, Aug. 1995. Morgan Kaufmann.Google Scholar
  4. 4.
    R. Caferra and N. Zabel. A method for simultanous search for refutations and models by equational constraint solving. Journal of Symbolic Computation, 13:613–642, 1992.zbMATHMathSciNetCrossRefGoogle Scholar
  5. 5.
    H. Chu and D. Plaisted. CLIN-S-a semantically guided first-order theorem prover. Journal of Automated Reasoning, 18(2):183–188, 1997.CrossRefGoogle Scholar
  6. 6.
    H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Preliminary version from October, 14 1999, available at:
  7. 7.
    N. Dershowitz and D. Plaisted. Rewriting. In J. Robinson and A. Voronkov, eds., Handbook of Automated Reasoning, volume 1, chapter 9, pp. 535–610. Elsevier and MIT Press, 2001.Google Scholar
  8. 8.
    C. G. Fermüller and A. Leitsch. Hyperresolution and automated model building. Journal of Logic and Computation, 6(2):173–230, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    C. G. Fermüller and A. Leitsch. Decision procedures and model building in equational clause logic. Logic Journal of the IGPL, 6(1):17–41, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Z. Fülöp and S. Vágvölgyi. Ground term rewriting rules for the word problem of ground term equations. Bulletin of the European Association for Theoretical Computer Science, 45:186–201, Oct. 1991.Google Scholar
  11. 11.
    G. Gottlob and R. Pichler. Hypergraphs in model checking: Acyclicity and hypertree-width versus clique-width. In F. Orejas, P. Spirakis, and J. Leeuwen, eds., Proc. 28th International Colloquium on Automata, Languages and Programming (ICALP’01), LNCS 2076, pp. 708–719, Crete, Greece, July 201. Springer-Verlag.CrossRefGoogle Scholar
  12. 12.
    B. Gramlich and R. Pichler. Algorithmic aspects of Herbrand models represented by ground atoms with ground equations. Technical report, Institut für Computersprachen, TU Wien, May 2002. Full version of this paper.Google Scholar
  13. 13.
    K. Hodgson and J. Slaney. System description: Scott-5. In R. Goré, A. Leitsch, and T. Nipkow, eds., Proc. 1st Int. Joint Conf. on Automated Reasoning (IJCAR’01), LNAI 2083, pp. 443–447, Siena, Italy, June 2001. Springer-Verlag.Google Scholar
  14. 14.
    R. Matzinger. Comparing computational representations of Herbrand models. In G. Gottlob, A. Leitsch, and D. Mundici, eds., Proc. 5th Kurt Gödel Colloquium-Computational Logic and Proof Theory (KGC’97), LNCS 1289, pp. 203–218, Vienna, Austria, Aug. 1997. Springer-Verlag.Google Scholar
  15. 15.
    R. Matzinger. Computational Representations of Models in First-Order Logic. PhD thesis, Vienna University of Technology, 2000.Google Scholar
  16. 16.
    N. Peltier. Tree automata and automated model building. Fundamenta Informaticae, 30(1):59–81, 1997.zbMATHMathSciNetGoogle Scholar
  17. 17.
    D. Plaisted and A. Sattler-Klein. Proof lengths for equational completion. Information and Computation, 125(2):154–170, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    H. Seidl. Deciding equivalence of finite tree automata. SIAM Journal on Computing,, 19(3):424–437, June 1990.Google Scholar
  19. 19.
    J. Slaney. FINDER: Finite domain enumerator-system description. In A. Bundy, ed., Proc. 12th Int. Conf. on Automated Deduction (CADE’94), LNAI 814, pp. 798–801, Nancy, France, June 26-July 1 1994. Springer-Verlag.Google Scholar
  20. 20.
    W. Snyder. A fast algorithm for generating reduced ground rewriting systems from a set of ground equations. Journal of Symbolic Computation, 15:415–450, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    T. Tammet. Resolution Methods for Decision Problems and Finite Model Building. PhD thesis, Chalmers University of Technology, Göteborg, Sweden, 1992.Google Scholar
  22. 22.
    S. Winker. Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions. Journal of the ACM, 29(2):273–284, 1982.zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    J. Zhang and H. Zhang. System description: Generating models by SEM. In M. McRobbie and J. Slaney, eds., Proc. 13th Int. Conf. on Automated Deduction (CADE’96), LNAI 1104, pp. 308–312, New Brunswick, NJ, USA, July 30-August 3 1996. Springer-Verlag.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Bernhard Gramlich
    • 1
  • Reinhard Pichler
    • 1
  1. 1.Inst. f. Computersprachen, AG Theoretische Informatik und LogikTechnische Universität WienWienAustria

Personalised recommendations