ModGen: Theorem Proving by Model Generation

ModGen (Model Generation) is a complete theorem prover for first order logic with finite Herbrand do- Sun Kim Hantao L&hang Department of Computer Science The University of Iowa Iowa City, IA 52242, U. S. A {sunkim, hihang}@cs. uiowa. edu mains. 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. Mod- Gen is easy to use and very efficient. Many problems which are hard for general resolution theorem provers are found easy for ModGen.

Authors

• Sun Kim Interdisciplinary Program in Bioinformatics, Seoul National University AIGENDRUG Co., Ltd. Department of Computer Science and Engineering, Seoul National University Interdisciplinary Program in Artificial Intelligence, Seoul National University

Keywords

No keywords are indexed for this paper.