Skip to main content
SpringerLink
Log in

System description generating models by SEM

  • Session 4B
  • Conference paper
  • First Online:
Book cover Automated Deduction — Cade-13 (CADE 1996)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1104))

Included in the following conference series:

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

On leave from the Software Institute, Academia Sinica, Beijing 100080, P.R.China

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. Fujita, M., Slaney, J., and Bennett, F.; “Automatic generation of some results in finite algebra,” Proc. IJCAI-93, 52–57, Chambéry, France.

    Google Scholar 

  2. Jech, T., “OTTER experiments in a system of combinatory logic,” J. Automated Reasoning 14 (1995) 413–426.

    Article  Google Scholar 

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

    Google Scholar 

  4. Kunen, K., “Single axioms for groups,” J. Automated Reasoning 9 (1992) 291–308.

    Article  Google Scholar 

  5. Manthey, R., and Bry, F., “SATCHMO: A theorem prover implemented in Prolog,” Proc. CADE-9 (1988) 415–434.

    Google Scholar 

  6. 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 

  7. Slaney, J., “FINDER: Finite domain enumerator — system description,” Proc. CADE-12 (1994) 798–801.

    Google Scholar 

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

    Article  Google Scholar 

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

    Google Scholar 

  10. Zhang, J., “Constructing finite algebras with FALCON,” accepted by J. Automated Reasoning.

    Google Scholar 

  11. Zhang, J., and Zhang, H., “SEM: a System for Enumerating Models,” Proc. IJCAI-95, 298–303.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The 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

M. A. McRobbie J. K. Slaney

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zhang, J., Zhang, H. (1996). System description generating models by SEM. In: McRobbie, M.A., Slaney, J.K. (eds) Automated Deduction — Cade-13. CADE 1996. Lecture Notes in Computer Science, vol 1104. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61511-3_96

Download citation

  • DOI: https://doi.org/10.1007/3-540-61511-3_96

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61511-8

  • Online ISBN: 978-3-540-68687-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation