Skip to main content
SpringerLink
Log in

Constraint propagation in model generation

  • Computational Logic
  • Conference paper
  • First Online:
Principles and Practice of Constraint Programming — CP '95 (CP 1995)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 976))

Abstract

Model generation refers to the automatic construction of models of a given logical theory. It can be regarded as a special case of constraint satisfaction where the constraints are a set of clauses with equality and functions. In this paper, we study various constraint propagation rules for finite model generation. We implemented these rules in a prototype system called SEM (a System for Enumerating Models). By experimenting with SEM, we try to identify a set of transformation rules that are both efficient and easy to implement. We also compare several existing model generation systems that are based on different logics and strategies.

Partially supported by the National Science Foundation under Grants CCR-9202838 and CCR-9357851.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bibel, W., “Constraint satisfaction from a deductive viewpoint,” Artificial Intelligence 35 (1988) 401–413.

    MathSciNet  Google Scholar 

  2. Bourely, C., Caferra, R., and Peltier, N., “A method for building models automatically: Experiments with an extension of OTTER,” Proc. 12th Conf. on Automated Deduction (CADE-12), Springer LNAI 814 (1994) 72–86.

    Google Scholar 

  3. Davis, M., and Putnam, H., “A computing procedure for quantification theory,” J. ACM 7 (1960) 201–215.

    Article  Google Scholar 

  4. Fujita, M., Slaney, J., and Bennett, F., “Automatic generation of some results in finite algebra,” Proc. 13th IJCAI (1993) 52–57.

    Google Scholar 

  5. Hasegawa, R., Koshimura, M., and Fujita, H., “MGTP: A parallel theorem prover based on lazy model generation,” Proc. 11th Conf. on Automated Deduction (CADE-11) Springer LNAI 607 (1992) 776–780.

    Google Scholar 

  6. Jaffar, J., and Maher, M.J., “Constraint logic programming: A survey,” J. of Logic Programming 19/20 (1994) 503–581.

    Article  Google Scholar 

  7. Kim, S., and Zhang, H., “ModGen: Theorem proving by model generation,” Proc. AAAI-94, Seattle (1994) 162–167.

    Google Scholar 

  8. Kumar, V., “Algorithms for constraint satisfaction problems: A survey,” AI Magazine 13 (1992) 32–44.

    Google Scholar 

  9. Lee, S.-J., and Plaisted, D. A., “Problem solving by searching for models with a theorem prover,” Artificial Intelligence 69 (1994) 205–233.

    MathSciNet  Google Scholar 

  10. Mackworth, A.K., “The logic of constraint satisfaction,” Artificial Intelligence 58 (1992) 3–20.

    MathSciNet  Google Scholar 

  11. Manthey, R., and Bry, F., “SATCHMO: A theorem prover implemented in Prolog,” Proc. 9th Conf. on Automated Deduction (CADE-9), LNCS 310 (1988) 415–434.

    Google Scholar 

  12. McCune, W., “Single axioms for groups and Abelian groups with various operations,” J. of Automated Reasoning 10 (1993) 1–13.

    Article  Google Scholar 

  13. McCune, W., “A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems,” Technical Report ANL/MCS-TM-194, Argonne National Laboratory (1994).

    Google Scholar 

  14. Slaney, J., “FINDER: Finite domain enumerator. Version 3.0 notes and guide,” Australian National University (1993).

    Google Scholar 

  15. Slaney, J., Stickel, M., and Fujita, M., “Automated reasoning and exhaustive search: Quasigroup existence problems,” Computers and Mathematics with Applications 29 (1995).

    Google Scholar 

  16. Tammet, T., ‘Using resolution for deciding solvable classes and building finite models,’ Baltic Computer Science: Selected Papers, Springer LNCS 502 (1991) 33–64.

    Google Scholar 

  17. Wos, L., Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, New Jersey (1988).

    Google Scholar 

  18. Wos, L., and McCune, W., “Negative paramodulation,” Proc. 8th Conf. on Automated Deduction (CADE-8), Springer LNCS 230 (1986) J.H. Siekmann (ed.) 229–239.

    Google Scholar 

  19. Zhang, H. and Stickel, M., “Implementing the Davis-Putnam algorithm by tries,” Technical Report, University of Iowa (1994).

    Google Scholar 

  20. Zhang, J., “Constructing finite algebras with FALCON,” J. of Automated Reasoning, to appear.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Iowa, 52242, Iowa City, IA, USA

    Jian Zhang & Hantao Zhang

Authors
  1. Jian Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hantao Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ugo Montanari Francesca Rossi

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zhang, J., Zhang, H. (1995). Constraint propagation in model generation. In: Montanari, U., Rossi, F. (eds) Principles and Practice of Constraint Programming — CP '95. CP 1995. Lecture Notes in Computer Science, vol 976. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60299-2_24

Download citation

  • DOI: https://doi.org/10.1007/3-540-60299-2_24

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60299-6

  • Online ISBN: 978-3-540-44788-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation