Willow : extending Herby's semantic tree theorem-proving heuristics
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...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Others |
| Language: | en |
| Published: |
McGill University
1999
|
| Subjects: | |
| Online Access: | http://digitool.Library.McGill.CA:80/R/?func=dbin-jump-full&object_id=21586 |