| Creator |
|
|
|
|
|
|
|
| Language |
|
| Publisher |
|
|
|
| Date |
|
| Source Title |
|
| Vol |
|
| Issue |
|
| First Page |
|
| Last Page |
|
| Publication Type |
|
| Access Rights |
|
| JaLC DOI |
|
| Related DOI |
|
| Related URI |
|
| Relation |
|
| Abstract |
We present a new method to eliminate redundant inferences caused by case-splitting in MGTP. There are two types of redundancies eliminated by the method: One is that the same sub-proof tree may be gen...erated at several descendant nodes after a case-splitting occurs. Another is caused by useless model candidate extensions with irrelevant non-Horn clauses. Both types of redundancies can be eliminated by combining the folding-up function that conveys unit lemmata obtained from solved descendant nodes to a proper antecedent node and the NHM function that suppresses useless model extensions. The method has been implemented in MGTP. We evaluate its effects on a UNIX workstation for some typical problems taken from the TPTP problem library.show more
|
Export Mendeley
p075