Mace4 reference manual and guide [electronic resource].
- Published
- Washington, D.C. : United States. Dept. of Energy, 2003.
Oak Ridge, Tenn. : Distributed by the Office of Scientific and Technical Information, U.S. Dept. of Energy. - Physical Description
- 20 pages : digital, PDF file
- Additional Creators
- Argonne National Laboratory, United States. Department of Energy, and United States. Department of Energy. Office of Scientific and Technical Information
Access Online
- Restrictions on Access
- Free-to-read Unrestricted online access
- Summary
- Mace4 is a program that searches for finite models of first-order formulas. For a given domain size, all instances of the formulas over the domain are constructed. The result is a set of ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied. If satisfiability is detected, one or more models are printed. Mace4 is a useful complement to first-order theorem provers, with the prover searching for proofs and Mace4 looking for countermodels, and it is useful for work on finite algebras. Mace4 performs better on equational problems than did our previous model-searching program Mace2.
- Report Numbers
- E 1.99:anl/mcs-tm-264
anl/mcs-tm-264 - Subject(s)
- Other Subject(s)
- Note
- Published through SciTech Connect.
10/27/2003.
"anl/mcs-tm-264"
McCune, W. - Type of Report and Period Covered Note
- Topical;
- Funding Information
- W-31-109-ENG-38
View MARC record | catkey: 14346013