Division of Informatics
Forrest Hill & 80 South Bridge
MSc Thesis #94110 | |
|---|---|
| Title: | An Exploration of Semantic Resolution |
| Authors: | Dennis,L |
| Date: | 1994 |
| Presented: | |
| Keywords: | |
| Abstract: | Semantic resolution is a suggested refinement of Robinson's resolution method for automatic theorem proving [Robinson 65]. It involves the use of models or interpretations to guide the search for a refutation. Several variants of semantic resolution exist, some of which are only complete for Horn sets. The implementation and testing of two variants, Semantic Lush and Semantic Clash resolutions, is described. The performance of both variants with Horn sets was disappointing and some possible reasons for this are suggested. These reasons implied that the performance might well improve as harder problems were tried. The performance of Semantic Clash resolution on non-Horn sets was much more promising than it had been on Horn sets and did indeed appear to be an improvement over the non-semantic methods examined. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}