- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- The linear resolution theorem prover
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
The linear resolution theorem prover Chan, Nelson Hin-Fai
Abstract
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 Metadata
| Title |
The linear resolution theorem prover
|
| Creator | |
| Publisher |
University of British Columbia
|
| Date Issued |
1984
|
| Description |
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.
|
| Genre | |
| Type | |
| Language |
eng
|
| Date Available |
2010-05-10
|
| Provider |
Vancouver : University of British Columbia Library
|
| Rights |
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.
|
| DOI |
10.14288/1.0051861
|
| URI | |
| Degree | |
| Program | |
| Affiliation | |
| Degree Grantor |
University of British Columbia
|
| Campus | |
| Scholarly Level |
Graduate
|
| Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
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.