Mace4 Reference Manual and Guide
Mace4 Reference Manual and Guide
复制标题
Mace4 参考手册和指南
DOI：
10.2172/822574
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
W. McCune
中科院分区：
文献类型：
--
作者：
W. McCune
MACE4是一个搜索一阶公式的有限模型的程序。对于给定的域大小，构建了域上公式的所有实例。结果是一组平等的地面条款。然后，应用基于地面方程重写的决策程序。如果检测到令人满意，则打印一个或多个型号。 MACE4是对一阶定理掠夺者的有用补充，供者搜索证明和MACE4寻找反模型，并且对于在有限代数上的工作非常有用。 MACE4在方程问题上的性能要比我们以前的模型搜索程序MACE2更好。
Mace4 is a program that searches for finite models of first-order formulas. For a given domain size, all instances of the formulas over the domain are constructed. The result is a set of ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied. If satisfiability is detected, one or more models are printed. Mace4 is a useful complement to first-order theorem provers, with the prover searching for proofs and Mace4 looking for countermodels, and it is useful for work on finite algebras. Mace4 performs better on equational problems than did our previous model-searching program Mace2.