The linear resolution theorem prover
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...
| Main Author: | |
|---|---|
| Language: | English |
| Published: |
University of British Columbia
2010
|
| Online Access: | http://hdl.handle.net/2429/24560 |