mace2(1) [debian man page]
MACE2(1) General Commands Manual MACE2(1) 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 proce- dure decides the propositional problem, and any models found are translated to first-order models. mace2 is a useful complement to the the- orem 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). November 5, 2006 MACE2(1)
Check Out this Related Man Page
Config::Model::models::LCDd(3pm) User Contributed Perl Documentation Config::Model::models::LCDd(3pm) NAME
Config::Model::models::LCDd - Configuration class LCDd VERSION
version 2.021 DESCRIPTION
Configuration classes used by Config::Model LCDd.conf -- configuration file for the LCDproc server daemon LCDd This file contains the configuration for the LCDd server. The format is ini-file-like. It is divided into sections that start at markers that look like [section]. Comments are all line-based comments, and are lines that start with ' The server has a 'central' section named [server]. For the menu there is a section called [menu]. Further each driver has a section which defines how the driver acts. The drivers are activated by specifying them in a driver= line in the server section, like: Driver=curses This tells LCDd to use the curses driver. The first driver that is loaded and is capable of output defines the size of the display. The default driver to use is curses. If the driver is specified using the -d <driver> command line option, the Driver= options in the config file are ignored. The drivers read their own options from the respective sections. Model information extracted from template /etc/LCDd.conf BUGS
This model does not support to load several drivers. Loading several drivers is probably a marginal case. Please complain to the author if this assumption is false Elements server Optional. Type node. menu Optional. Type node. bayrad Optional. Type warped_node. CFontz Optional. Type warped_node. CFontzPacket Optional. Type warped_node. curses Optional. Type warped_node. CwLnx Optional. Type warped_node. ea65 Optional. Type warped_node. EyeboxOne Optional. Type warped_node. g15 Optional. Type warped_node. glcd Optional. Type warped_node. glcdlib Optional. Type warped_node. glk Optional. Type warped_node. hd44780 Optional. Type warped_node. icp_a106 Optional. Type warped_node. IOWarrior Optional. Type warped_node. imon Optional. Type warped_node. imonlcd Optional. Type warped_node. IrMan Optional. Type warped_node. irtrans Optional. Type warped_node. joy Optional. Type warped_node. lb216 Optional. Type warped_node. lcdm001 Optional. Type warped_node. lcterm Optional. Type warped_node. lirc Optional. Type warped_node. lis Optional. Type warped_node. MD8800 Optional. Type warped_node. mdm166a Optional. Type warped_node. ms6931 Optional. Type warped_node. mtc_s16209x Optional. Type warped_node. MtxOrb Optional. Type warped_node. mx5000 Optional. Type warped_node. NoritakeVFD Optional. Type warped_node. picolcd Optional. Type warped_node. pyramid Optional. Type warped_node. sed1330 Optional. Type warped_node. sed1520 Optional. Type warped_node. serialPOS Optional. Type warped_node. serialVFD Optional. Type warped_node. shuttleVFD Optional. Type warped_node. stv5730 Optional. Type warped_node. SureElec Optional. Type warped_node. svga Optional. Type warped_node. text Optional. Type warped_node. t6963 Optional. Type warped_node. tyan Optional. Type warped_node. ula200 Optional. Type warped_node. sli Optional. Type warped_node. vlsys_m428 Optional. Type warped_node. xosd Optional. Type warped_node. SEE ALSO
o cme o Config::Model::models::LCDd::CFontz o Config::Model::models::LCDd::CFontzPacket o Config::Model::models::LCDd::CwLnx o Config::Model::models::LCDd::EyeboxOne o Config::Model::models::LCDd::IOWarrior o Config::Model::models::LCDd::IrMan o Config::Model::models::LCDd::MD8800 o Config::Model::models::LCDd::MtxOrb o Config::Model::models::LCDd::NoritakeVFD o Config::Model::models::LCDd::SureElec o Config::Model::models::LCDd::bayrad o Config::Model::models::LCDd::curses o Config::Model::models::LCDd::ea65 o Config::Model::models::LCDd::g15 o Config::Model::models::LCDd::glcd o Config::Model::models::LCDd::glcdlib o Config::Model::models::LCDd::glk o Config::Model::models::LCDd::hd44780 o Config::Model::models::LCDd::icp_a106 o Config::Model::models::LCDd::imon o Config::Model::models::LCDd::imonlcd o Config::Model::models::LCDd::irtrans o Config::Model::models::LCDd::joy o Config::Model::models::LCDd::lb216 o Config::Model::models::LCDd::lcdm001 o Config::Model::models::LCDd::lcterm o Config::Model::models::LCDd::lirc o Config::Model::models::LCDd::lis o Config::Model::models::LCDd::mdm166a o Config::Model::models::LCDd::menu o Config::Model::models::LCDd::ms6931 o Config::Model::models::LCDd::mtc_s16209x o Config::Model::models::LCDd::mx5000 o Config::Model::models::LCDd::picolcd o Config::Model::models::LCDd::pyramid o Config::Model::models::LCDd::sed1330 o Config::Model::models::LCDd::sed1520 o Config::Model::models::LCDd::serialPOS o Config::Model::models::LCDd::serialVFD o Config::Model::models::LCDd::server o Config::Model::models::LCDd::shuttleVFD o Config::Model::models::LCDd::sli o Config::Model::models::LCDd::stv5730 o Config::Model::models::LCDd::svga o Config::Model::models::LCDd::t6963 o Config::Model::models::LCDd::text o Config::Model::models::LCDd::tyan o Config::Model::models::LCDd::ula200 o Config::Model::models::LCDd::vlsys_m428 o Config::Model::models::LCDd::xosd COPYRIGHT
2011, Dominique Dumont 1999-2011, William Ferrell and others LICENSE
GPL-2 perl v5.14.2 2012-11-09 Config::Model::models::LCDd(3pm)