We present a method embedding two mechanisms, which eliminate redundant inferences, into CMGTP. One is delayed relevancy testing which eliminates unnecessary subproofs by calculating relevancy to the proof. Another is folding-up which eliminates a duplicate subproof by using lemmas extracted from the proof. These two mechanisms are achieved by extracting literals that have contributed to the proof. We have implemented the method in Java and evaluated its effects for some typical problems taken from the TPTP problem library.
|Number of pages
|Research Reports on Information Science and Electrical Engineering of Kyushu University
|Published - Sept 1999
All Science Journal Classification (ASJC) codes
- Electrical and Electronic Engineering
- General Computer Science