Computation with run time skolemisation (N-Prolog part 3)
- 1 January 1993
- journal article
- research article
- Published by Taylor & Francis in Journal of Applied Non-Classical Logics
- Vol. 3 (1) , 93-128
- https://doi.org/10.1080/11663081.1993.10510797
Abstract
Two computation procedures are described for intuitionistic and classical logic. The first introduces Skolem functions at runtime. The second restricts unification by time stamping. For universal Horn clauses the computation is the same as Prolog.Keywords
This publication has 4 references indexed in Scilit:
- A family of goal directed theorem provers based on conjunction and implication: Part 1Journal of Automated Reasoning, 1991
- N-Prolog: An extension of prolog with hypothetical implication. II. Logical foundations, and negation as failureThe Journal of Logic Programming, 1985
- N-Prolog: An extension of Prolog with hypothetical implications. I.The Journal of Logic Programming, 1984
- Semantical Analysis of Intuitionistic Logic IPublished by Elsevier ,1965