Model Generation for Horn Logic with Stratified Negation

  • Ethan K. Jackson
  • Wolfram Schulte
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5048)


Model generation is an important formal technique for finding interesting instances of computationally hard problems. In this paper we study model generation over Horn logic under the closed world assumption extended with stratified negation. We provide a novel three-stage algorithm that solves this problem: First, we reduce the relevant Horn clauses to a set of non-monotonic predicates. Second, we apply a fixed-point procedure to these predicates that reveals candidate solutions to the model generation problem. Third, we encode these candidates into a satisfiability problem that is evaluated with a state-of-the-art SMT solver. Our algorithm is implemented, and has been successfully applied to key problems arising in model-based design.


Function Symbol Horn Clause Closed World Ground Term Proof Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Jackson, E.K., Sztipanovits, J.: Towards a formal foundation for domain specific modeling languages. In: Proceedings of the Sixth ACM International Conference on Embedded Software (EMSOFT 2006), pp. 53–62 (2006)Google Scholar
  2. 2.
    Object Management Group: Mda guide version 1.0.1. Technical report (2003)Google Scholar
  3. 3.
    Bezivin, J., Gerbé, O.: Towards a precise definition of the omg/mda framework. In: Proceedings of the 16th Conference on Automated Software Engineering, pp. 273–280 (2001)Google Scholar
  4. 4.
    Karsai, G., Sztipanovits, J., Ledeczi, A., Bapty, T.: Model-integrated development of embedded software. Proceedings of the IEEE 91(1), 145–164 (2003)CrossRefGoogle Scholar
  5. 5.
    Burch, J., Passerone, R., Sangiovanni-Vincentelli, A.: Modeling techniques in design-by-refinement methodologies. Integrated Design and Process Technology (June 2002)Google Scholar
  6. 6.
    Lee, E.A., Neuendorffer, S.: Actor-oriented models for codesign: Balancing re-use and performance. In: Formal Methods and Models for Systems. Kluwer, Dordrecht (2004)Google Scholar
  7. 7.
    Przymusinski, T.C.: Every logic program has a natural stratification and an iterated least fixed point model. In: PODS 1989: Proceedings of the eighth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, pp. 11–21. ACM, New York (1989)CrossRefGoogle Scholar
  8. 8.
    Jensen, T.R., Toft, B.: Graph Coloring Problems. Wiley-Interscience, New York, ISBN 0-471-02865-7Google Scholar
  9. 9.
    Reiter, R.: On closed world data bases, pp. 300–310 (1987)Google Scholar
  10. 10.
    Blass, A., Gurevich, Y.: Existential fixed-point logic. In: Börger, E. (ed.) Computation Theory and Logic. LNCS, vol. 270, pp. 20–36. Springer, Heidelberg (1987)CrossRefGoogle Scholar
  11. 11.
    van Gelder, A., Ross, K., Schlipf, J.S.: The well-founded semantics for general logic programs. Journal of the ACM 38, 620–650 (1991)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R.A., Bowen, K. (eds.) Proceedings of the Fifth International Conference on Logic Programming, pp. 1070–1080. The MIT Press, Cambridge (1988)Google Scholar
  13. 13.
    Marek, V.W., Nerode, A., Remmel, J.B.: A context for belief revision: Forward chaining - normal nonmonotonic rule systems. Ann. Pure Appl. Logic 67(1-3), 269–323 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Emden, M.H.V., Kowalski, R.A.: The semantics of predicate logic as a programming language. J. ACM 23, 733–742 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Apt, K.R., Doets, K.: A new definition of SLDNF-resolution. The Journal of Logic Programming 18, 177–190 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Dantsin, E., Eiter, T., Gottlob, G., Voronkov, A.: Complexity and expressive power of logic programming. ACM Comput. Surv. 33(3), 374–425 (2001)CrossRefGoogle Scholar
  17. 17.
    de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Proceedings of Fourteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • Ethan K. Jackson
    • 1
  • Wolfram Schulte
    • 1
  1. 1.Microsoft ResearchRedmondUSA

Personalised recommendations