MACE 2.0 Reference Manual and Guide
计算机科学中的逻辑
2007-05-23 v1 符号计算
摘要
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.
引用
@article{arxiv.cs/0106042,
title = {MACE 2.0 Reference Manual and Guide},
author = {William McCune},
journal= {arXiv preprint arXiv:cs/0106042},
year = {2007}
}
备注
10 pages