Name
Abstract | ||
|---|---|---|
This paper describes a number of heuristics that have been implemented in a program that proves theorems by constructing closed semantic trees. The program is called HERBY. We studied the effectiveness of these heuristics on the Stickel Test Set and found that when HERBY was given two hours to prove each theorem, it was able to prove 78 of the 84 theorems in the set. Constructing semantic trees has been used as a theoretical tool for confirming the unsatisfiability of a set of clauses in first‐order predicate calculus; this paper shows that this approach has some practicality as well. |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1023/A:1018976510663 | Ann. Math. Artif. Intell. |
Keywords | Field | DocType |
Terminal Node,Theorem Prove,Failure Node,Automate Theorem Prove,Unit Clause | Discrete mathematics,Automated theorem proving,Heuristics,Predicate (grammar),Mathematics,Test set | Journal |
Volume | Issue | ISSN |
23 | 3-4 | 1573-7470 |
Citations | PageRank | References |
3 | 0.54 | 5 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Qingxun Yu | 1 | 3 | 0.54 |
| Mohammed Almulla | 2 | 147 | 20.60 |
| Monroe M. Newborn | 3 | 177 | 47.49 |