A declarative semantics for Prolog propositional programs with negation by failure can be obtained by extending the modal system G of arithmetical provability [see, e.g., G. Boolos, The unprovability of consistency, Cambridge Univ. Press, Cambridge, 1979] to a bi-modal system L. L is proved to be sound and complete for the class of Kripke models with the following L-tree structure: (a) An L-tree contains at least two nodes; (b) for every atom A, if A is true [false] at all non-endpoints, then A is true [false] at all endpoints as well.
A complete bi-modal system for a class of models
TERRACINI, Lea
1988-01-01
Abstract
A declarative semantics for Prolog propositional programs with negation by failure can be obtained by extending the modal system G of arithmetical provability [see, e.g., G. Boolos, The unprovability of consistency, Cambridge Univ. Press, Cambridge, 1979] to a bi-modal system L. L is proved to be sound and complete for the class of Kripke models with the following L-tree structure: (a) An L-tree contains at least two nodes; (b) for every atom A, if A is true [false] at all non-endpoints, then A is true [false] at all endpoints as well.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
