Name
Abstract | ||
|---|---|---|
In this paper, we investigate the practicality of generating semantic trees to prove the unsatisfiability of sets of clauses in first-order predicate logic. Two methods of generating semantic trees are considered. First, we consider semantic trees generated by using the canonical enumeration of Herbrand base atoms. Then, we consider semantic trees generated by selectively choosing the atoms from the Herbrand base. A comparison is made between the two approaches using the theorems from the Stickel Test Set. |
Year | DOI | Venue |
|---|---|---|
1996 | 10.1080/00207169608804524 | INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS |
Keywords | Field | DocType |
Herbrand universe, Herbrand base, unsatisfiability, Herbrand interpretation, Herbrand procedure, semantic trees | Discrete mathematics,Mathematical optimization,Enumeration,Theoretical computer science,Semantic network,Mathematical proof,First-order logic,Herbrand interpretation,Predicate logic,Mathematics,Test set | Journal |
Volume | Issue | ISSN |
62 | 1-2 | 0020-7160 |
Citations | PageRank | References |
2 | 0.41 | 7 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mohammed Almulla | 1 | 147 | 20.60 |
| Monroe M. Newborn | 2 | 177 | 47.49 |