(11) Development of an MGTP System on KLIC

MGTP is a model-generation based theorem prover for first-order logic. The implementation language of MGTP is KL1 which is complied into C language by the KLIC system. MGTP incorporates several functions to enhance proving efficiency. The folding-up and NHM operations eliminate redundant inferences caused by case-splittings in MGTP. The merc- and rams-methods eliminate redundant computations in conjunctive matching which would be a primary cause of significant speed-down of the model-generation based theorem provers. Discrimination-tree indexing is available for the retrieval operation to find terms that unify with a given term. These functions improve the performance of MGTP significantly. CMGTP is a slightly modified version of MGTP, enabling negative constraint propagation. CMGTP can be used as a general constraint solver for problems on finite-domains. An MGTP window manager is available for providing a user-friendly graphical user interface.