This paper presents a new constructive form of the negation-as-failure rule dedicated to concurrent executions and, based on it, a parallel execution model of general Horn clauses. Referring to the completion understanding of the programs, this model has been proved sound and as complete as possible when the resolution rule and the negation-as-failure rule are used. Furthermore, it does not suffer from the floundering problem: in contrast, negative literals can be used to produce computed answers as the positive literals can. This new form of negation is based on an equational framework. It introduces generalizations of substitutions, terms and related concepts of instantiation and unification. A theory of such concepts is also presented in the paper.

, , ,
doi.org/10.1007/3-540-55437-8_88
International Conference of the Austrian Center for Parallel Computation
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Jacquet, J.-M. (1991). Negation in Conclog. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 289–315). doi:10.1007/3-540-55437-8_88