| 3 | | HOPES is a prototype interpreter written in [http://www.haskell.org/haskellwiki/Haskell Haskell] for the definitorial higher order [http://en.wikipedia.org/wiki/Prolog PROLOG]. |
| 4 | | The interpreter implements a higher order proof procedure with extensional semantics. |
| | 3 | Hopes is a prototype interpreter for a higher-order PROLOG-like |
| | 4 | language. The syntax of the language extends that of [http://en.wikipedia.org/wiki/Prolog PROLOG] by |
| | 5 | supporting higher-order constructs (such as higher-order predicate |
| | 6 | variables, partial application and lambda terms). In particular, |
| | 7 | the syntax allows clauses (and queries) that contain uninstantiated |
| | 8 | predicate variables. The interpreter implements a higher-order |
| | 9 | top-down SLD-resolution proof procedure described in [http://arxiv.org/abs/1106.3457 this paper]. In the |
| | 10 | case of uninstantiated predicate variables, the proof procedure |
| | 11 | will systematically (and in a sophisticated way) investigate all |
| | 12 | finite instantiations of these variables. |
