UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

The linear resolution theorem prover Chan, Nelson Hin-Fai


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.

Item Media

Item Citations and Data


For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.