Direct finite first-order model generation with negative constraint propagation heuristic

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Direct finite first-order model generation with negative constraint propagation heuristic

Full text

Pdf (468 KB)

Source

Symposium on Applied Computing archive
Proceedings of the 1997 ACM symposium on Applied computing table of contents

San Jose, California, United States

Pages: 25 - 29

Year of Publication: 1997

ISBN:0-89791-850-9

Authors

Olga Shumsky	Department of Electrical and Computer Engineering, Northwestern University, Evanston, Illinois
Ralph W. Wilkerson	Department of Computer Science, University of Missouri-Rolla, Rolla, Missouri
William W. McCune	Mathematics and Computer Science Division, Argonne National Laboratory, 9700 South Cass Avenue, Argonne, Illinois
Fikret Ercal	Department of Computer Science, University of Missouri-Rolla, Rolla, Missouri

Sponsors

SIGCUE: ACM Special Interest Group on Computer Uses In Education
SIGADA: ACM Special Interest Group on Ada Programming Language
SIGAPP: ACM Special Interest Group on Applied Computing
SIGBIO: ACM Special Interest Group on Biomedical Computing

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 0, Downloads (12 Months): 10, Citation Count: 0

Additional Information:

references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/331697.331704 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	F. E. Bennett and L. Zhu. Conjugate-orthogonal latin squares and related structures. In Jeffrey H. Dinitz and Douglas R. Stinson, editors, Contemporary Design Theory: A Collection of Surveys, pages 41-96. John Wiley & Sons, Inc., 1992.
	2	Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
	3	Jun Gu. Local search for satisfiablity (SAT) problem. IEEE Transactions on Systems, Man, and Cybernetics, 23(4):1108-1129, 1993.
	4	John McCarthy. A tough nut for proof procedures. Stanford Artificial Intelligence Project, July 1964.
	5	William W. McCune. A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems. Argonne National Laboratory, September 1994.
	6	J. Slaney, M. Fujita, and M. Stickel. Automated reasoning and exhaustive search: quasigroup existence problems. Computers and Mathematics with Applications, 29(2):115-132, 1995.
	7	J. Stanley. F~NDEa version 3.0 notes and guide. Centre for Information Science Research, Australian National University, 1993.
	8	Hantao Zhang and Mark E. Stickel. Implementing the Davis-Putnam algorithm by tries. University of Iowa, 1994.
	9	Jian Zhang and Hantao Zhang. SEM: a system for enumerating models. In Fourteenth International Joint Conference on Artificial Intelligence, pages 298-303, 1995.
	10	Jian Zhang and Hantao Zhang. SEM user guide. Department of Computer Science, University of Iowa, 1995.
	11	Jian Zhang and Hantao Zhang. Combining local search and backtracking techniques for constraint satisfaction. Forthcoming, 1996.
	12	Jian Zhang and Hantao Zhang. The model generator SEM (system description). Forthcoming, 1996.