.TH MACE2 1 "November 5, 2006" .SH NAME mace2 \- searches for finite countermodels of first-order statements .SH SYNOPSIS .B mace2 .RI [ options ] < .I input-file > .I output-file .SH DESCRIPTION This manual page documents briefly the .B mace2 command. .PP \fBmace2\fP is a program that searches for finite models of first-order statements. The statement to be modeled is first translated to clauses, then to relational clauses; finally for the given domain size, the ground instances are constructed. A Davis-Putnam-Loveland-Logeman procedure decides the propositional problem, and any models found are translated to first-order models. \fBmace2\fP is a useful complement to the theorem prover .BR otter (1), with \fBotter\fP searching for proofs and \fBmace2\fP looking for countermodels. .SH OPTIONS A summary of options is included below. .TP .B \-n \fIn This gives the starting domain size for the search. The default value is 2. If you also give an \fB-N\fP option, MACE will iterate domain sizes up through the \fB-N\fP value. Otherwise, \fBmace2\fP will search only for the \fB-n\fP value. .TP .B \-N \fIn This gives the ending domain size for the search. The default is the value of the \fB-n\fP option. .TP .B \-c This says that constants in the input should be assigned unique elements of the domain. If the number of constants in the input is greater than the domain size \fIn\fP, the first \fIn\fP constants are given values, and the rest are unconstrained. This is a useful option because it eliminates lots of isomorphism from the search. But it can block all models, especially when used with other constraints. .TP .B \-p This option tells \fBmace2\fP to print models in a nice tabular form as they are found. This format is meant for human consumption. .TP .B \-P This option tells \fBmace2\fP to print models in an easily parsable form. This format has an \fBotter\fP-like syntax and can be read by most Prolog systems. .TP .B \-I This option tells \fBmace2\fP to print models in IVY form. This format is a Lisp S-expression and is meant to be read by IVY, our proof and model checker. .TP .B \-m \fIn This tells \fBmace2\fP to stop after finding \fIn\fP models. The default is 1. .TP .B \-t \fIn This tells \fBmace2\fP to stop after about n seconds. The default is unlimited. \fBmace2\fI ignores any assign(max_seconds, n) commands that might be in the input file. Such commands are used by \fBotter\fI only. .TP .B \-k \fIn This tells \fBmace2\fP to stop if it tries to allocate more than \fIn\fP kilobytes of memory. The default is 48000 (about 48 megabytes). \fBmace2\fI ignores any assign(max_mem, n) commands that might be in the input file. Such commands are used by \fBotter\fI only. .TP .B \-x This is a special-purpose constraint designed to reduce isomorphism in quasigroup problems. It applies only to binary function \fIf\fP. .TP .B \-h This tells \fBmace2\fP to print a summary of these command-line options. .SH SEE ALSO .BR anldp (1), .BR formed (1), .BR otter (1), .BR pl (1). .br Full documentation for \fBmace2\fP is found in \fI/usr/share/doc/mace2/mace2.{html,ps.gz}\fP. .SH AUTHOR \fBmace2\fP ws written by William McCune .PP This manual page was written by Peter Collingbourne , for the Debian project (but may be used by others).