MACE 2.0 reference manual and guide.

McCune, W.

Argonne National Laboratory

关键词: Algorithms;    M Codes;    Manuals;    99 General And Miscellaneous//Mathematics, Computing, And Information Science;   

DOI  :  10.2172/797949
RP-ID  :  ANL/MCS-TM-249
RP-ID  :  W-31-109-ENG-38
RP-ID  :  797949

美国|英语

来源: UNT Digital Library

【 摘 要 】

MACE 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. MACE is a useful complement to the theorem prover Otter, with Otter searching for proofs and MACE looking for countermodels.