## Rechercher une page de manuel

# mace2

Langue: *en*

Version: *250237 (debian - 07/07/09)*

Section: *1 (Commandes utilisateur)*

## NAME

mace2 - searches for finite countermodels of first-order statements## SYNOPSIS

**mace2**[

*options*] <

*input-file*>

*output-file*

## DESCRIPTION

This manual page documents briefly the**mace2**command.

**mace2** 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. **mace2** is a useful complement to the theorem prover **otter**(1), with **otter** searching for proofs and **mace2** looking for countermodels.

## OPTIONS

A summary of options is included below.**-n***n*- This gives the starting domain size for the search. The default value is 2. If you also give an
**-N**option, MACE will iterate domain sizes up through the**-N**value. Otherwise,**mace2**will search only for the**-n**value. **-N***n*- This gives the ending domain size for the search. The default is the value of the
**-n**option. **-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
*n*, the first*n*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. **-p**- This option tells
**mace2**to print models in a nice tabular form as they are found. This format is meant for human consumption. **-P**- This option tells
**mace2**to print models in an easily parsable form. This format has an**otter**-like syntax and can be read by most Prolog systems. **-I**- This option tells
**mace2**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. **-m***n*- This tells
**mace2**to stop after finding*n*models. The default is 1. **-t***n*- This tells
**mace2**to stop after about n seconds. The default is unlimited.**mace2***ignores any assign(max_seconds, n) commands that might be in the input file. Such commands are used by***otter***only.* **-k***n*- This tells
**mace2**to stop if it tries to allocate more than*n*kilobytes of memory. The default is 48000 (about 48 megabytes).**mace2***ignores any assign(max_mem, n) commands that might be in the input file. Such commands are used by***otter***only.* **-x**- This is a special-purpose constraint designed to reduce isomorphism in quasigroup problems. It applies only to binary function
*f*. **-h**- This tells
**mace2**to print a summary of these command-line options.

## SEE ALSO

**anldp**(1),

**formed**(1),

**otter**(1),

**pl**(1).

Full documentation for

**mace2**is found in

*/usr/share/doc/mace2/mace2.{html,ps.gz}*.

## AUTHOR

**mace2**ws written by William McCune <otter@mcs.anl.gov>

This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, for the Debian project (but may be used by others).

Il faut craindre énormément de comprendre.

-+- Paul Valéry -+-

Contenus ©2006-2018 Benjamin Poulain

Design ©2006-2018 Maxime Vantorre