Analysis of the use of semantic trees in automated theorem proving
Semantic trees have served as a theoretical tool for confirming the unsatisfiability of clauses in first-order predicate logic, but it has seemed impractical to use them in practice. In this thesis we experimentally investigated the practicality of generating semantic trees for proofs of unsatisfiab...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Others |
| Language: | en |
| Published: |
McGill University
1994
|
| Subjects: | |
| Online Access: | http://digitool.Library.McGill.CA:80/R/?func=dbin-jump-full&object_id=28662 |