ModGen: Theorem proving by model generation. 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.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Lucas, Salvador: Proving semantic properties as first-order satisfiability (2019)
- de Nivelle, Hans: Theorem proving for classical logic with partial functions by reduction to Kleene logic (2017)
- Zhang, Hantao; Zhang, Jian: MACE4 and SEM: a comparison of finite model generators (2013)
- de Nivelle, Hans; Meng, Jia: Geometric resolution: a proof procedure based on finite model search (2006)
- Brisoux, Laure; Grégoire, Éric; Saïs, Lakhdar: Checking depth-limited consistency and inconsistency in knowledge-based systems (2001)
- Zhang, Jian; Zhang, Hantao: System description -- generating models by SEM (1996)