| Summary: | This thesis describes a first-order logic automated theorem prover named Willow. Like its predecessor Herby, Willow solves theorems by constructing closed semantic trees. The main goal of Willow is to facilitate the closure of semantic trees by incorporating techniques found useful in other theorem provers. Extensions include the handling of equality via demodulation and paramodulation, the use of free variables, the heavy use of hash tables, and the use of new inference rules. Willow also contains simplification operations such as the detection of unused and useless atoms, and the reuse of subsumed subtrees. Willow is integrated in a graphical user interface, and is currently available for Windows 95/NT and UNIX-like operating systems.
|
|---|
