The propositional formula checker HeerHugo
HeerHugo is a propositional formula checker that determines whether a given formula is satisfiable or not. Its main ingredient is the branch/merge rule, that is inspired by an algorithm proposed by Staa llmarck, which is protected by a software patent. The algorithm can be interpreted as a breadth first search algorithm. HeerHugo differs substantially from Staa llmarck's algorithm, as it operates on formulas in conjunctive normal form and it is enhanced with many logical rules including unit resolution, 2--satisfiability tests and additional systematic reasoning techniques In this paper, the main elements of the algorithm are discussed, and its remarkable effectiveness is illustrated with some examples and computational results.
|GENERAL (acm F.0), ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY (acm F.2), MATHEMATICAL LOGIC AND FORMAL LANGUAGES (acm F.4)|
|Classical propositional logic (msc 03B05), Theory of computing (msc 68Qxx), Theorem proving (deduction, resolution, etc.) (msc 68T15)|
|Software Engineering [SEN]|
Groote, J.F, & Warners, J.P. (1999). The propositional formula checker HeerHugo. Software Engineering [SEN]. CWI.