MACE4 and SEM: A Comparison of Finite Model Generators
MACE4 and SEM: A Comparison of Finite Model Generators
复制标题
MACE4 和 SEM：有限模型生成器的比较
DOI：
10.1007/978-3-642-36675-8_5
复制
发表时间：
2013
影响因子：
3.3
通讯作者：
Jian Zhang
中科院分区：
文献类型：
--
作者：
Hantao Zhang;Jian Zhang
这篇文章有三个目的：(1)推广Mace4，一个由Bill McCune开发的程序，用于搜索一阶公式的有限模型，这是记住Bill的最好方式。(2)推动一阶公式模型生成的研究。Mace4仍然是最好的模型生成程序之一，我们需要新人接替比尔的火炬，因为模型生成对自动推理非常重要，有很多应用。(3)将Mace4与SEM进行详细比较，以便这些工具的用户或新模型生成器开发人员了解这两个系统的优缺点，并从本研究中获益。
This article has three objectives: (1) Promote Mace4, a program developed by Bill McCune that searches for finite models of first-order formulas and that is the best way to remember Bill. (2) Promote the research on model generation of first-order formulas. Mace4 remains one of the best model generation programs and we need newcomers who can take over Bill's torch, because model generation is very important to automated reasoning and has many applications. (3) Compare Mace4 with SEM in detail so that the users of these tools or new model generator developers will understand the strengths and weaknesses of both systems and take advantage from this study.