| Summary: | A resolution-based theorem prover (LRTP) has been built on the PROLOG/MTS system. The LRTP is designed for studying the performance of three resolution strategies, namely, linear input resolution, linear resolution, and ordered linear deduction. It allows the user to perform experiments on the three strategies in combination with others. Furthermore, the user has control over the environment in which the theorem is proved. The number of unifications involved in the search for a proof is used as a measure of performance. === Science, Faculty of === Computer Science, Department of === Graduate
|
|---|
