ModGen: Theorem Proving by Model Generation
ModGen: Theorem Proving by Model Generation
复制标题
DOI：
--
复制
发表时间：
1994-08
期刊：
影响因子：
--
通讯作者：
Sun Kim;Hantao Zhang
中科院分区：
文献类型：
--
作者：
Sun Kim;Hantao Zhang
Modgen（模型生成）是具有有限Herbrand域的一阶逻辑的完整定理供台。 Modgen将一阶公式作为输入，并生成输入公式的模型。 Modgen由两个主要模块组成：将输入公式转换为命题子句的模块，以及一个查找命题子句模型的模块。第一个模块可以由其他研究人员使用，以便可以轻松地表示，存储和传达SAT问题。 Modgen设计的一个重要问题是，如果原始公式为原始公式，则可以满足转换的命题子句。第二个模块可以很容易被任何高级SAT问题解决方案所取代。 Modgen易于使用且非常有效。对于ModGen来说，很容易发现许多对于一般分辨率定理抛弃的问题。
ModGen (Model Generation) is a complete theorem prover for first order logic with finite Herbrand domains. ModGen takes first order formulas as input, and generates models of the input formulas. ModGen consists of two major modules: a module for transforming the input formulas into propositional clauses, and a module to find models of the propositional clauses. The first module can be used by other researchers so that the SAT problems can be easily represented, stored and communicated. An important issue in the design of ModGen is to ensure that transformed propositional clauses are satisfiable iff the original formulas are. The second module can be easily replaced by any advanced SAT problem solver. ModGen is easy to use and very efficient. Many problems which are hard for general resolution theorem provers are found easy for ModGen.