MOLOG: A system that extends PROLOG with modal logic (Q1079962)

The author's aim is to extend PROLOG with modal logic. The first step would be to use the corresponding resolution rule. A formulation for the propositional case was developed in the course of the correspondence between the reviewer and the author [cf.: \textit{G. E. Mints}, Vsesoyuznogo simpoziuma po kibernetike 2, 34-36 (1981); \textit{L. Fariñas del Cerro}, Inf. Process. Lett. 14, 49-51 (1982; Zbl 0515.03009)]. The author prefers here to use another formulation for (what he calls) modal Horn clauses. The proof of the (completeness) theorem 1 is only outlined and at least one of lemmas 1, 2 allowing to delete the necessity operator will probably be false under any reasonable definition of satisfiability. The paper is very difficult to read since many definitions are either absent or incomplete. No resolution-type formulation of the predicate S5 (with satisfactory completeness proof) is known to the reviewer, and it is not clear which one the author has in mind. At least his definition 11 (of resolution) does not take unifying substitution into account and no precise definition is given later. An obvious way to treat the completely modalised case (all atoms are preceded by the necessity sign) is simply to drop all modalities and use ordinary PROLOG. This can be justified by reference to the faithfulness and soundness of Tarski translation, but hardly can be called extension.