Topic: MOLOG - a tool for non-classical logic programming

Participants: Luis Fariñas del Cerro, Andreas Herzig

MOLOG has been developped by the Applied Logic Group at IRIT from 1985 on. It has been supported by the ESPRIT project ALPES. Based on the modal resolution method proposed by Luis Fariñas del Cerro, a first prototype of MOLOG has been written in 1985 by R. Arthaud. Subsequently P. Bieber has implemented improved C-Prolog versions in 1986 and 1988, adapted to other Prolog interpreters by J.-F. Bosc in 1992. The principles of an abstract machine have been elaborated by M. Bricard in 1987. This work has been continued by J. Garmendia Aguirre and J.-M. Alliot and has led the latter to implementations in ADA and C in 1991.

MOLOG is a general inference machine for building a large class of meta-interpreters. It is in particular suitable for implementing extensions of Prolog with non-classical logics such as logics of knowledge, belief, time, action, uncertainty, etc. MOLOG handles Prolog clauses (with conjunctions & and implications <--) qualified by modal operators , such as pos:it_rains (it is possible that it rains), or knows(a):pos:it_rains (agent a knows that it is possible that it rains). The user has the possibility to define his modal operators. The language can be multi-modal (i.e., contain several modal operators at the same time).

Classical resolution is extended with modal resolution rules that define the operations that can be performed on the modal operators. These rules depend on the modal logic. The MOLOG user can either use an already existing set of resolution rules, or create his own set of rules.

The MOLOG implementation that is available is a metainterpreter written in C_Prolog. The interpreter currently runs on C-Prolog, Quintus-Prolog, Sicstus-Prolog, and SWI-Prolog.

Papers on MOLOG
Download MOLOG (20 K)
Description of the package
How to use MOLOG

Questions and remarks to Andreas Herzig

Papers on MOLOG

R. Arthaud, P. Bieber, L. Fariñas del Cerro, J. Henry, A. Herzig (1986), Automated modal reasoning.
Proc. Int. Conf. on Information Processing and Management of Uncertainty in Knowledge-Baseed Systems (IPMU-86), Springer Verlag, LNCS.
(first version of MOLOG)
L. Fariñas del Cerro (1986), MOLOG: a system that extends Prolog with modal logic.
The New Generation Computer Journal 4, pp 35-50.
(description of the inference rules for several modal logics)
L. Fariñas del Cerro, M. Penttonen (1987), A note on the complexity of the satisfiability of modal Horn clauses.
The Journal of Logic Programming, march 1987.
(complexity results for modal logic programming)
P. Bieber, L. Fariñas del Cerro, A. Herzig (1988), MOLOG: A modal Prolog.
Proc. Int. Conf. on Automated Deduction (CADE-88), Springer Verlag, LNCS 310.
(short description of MOLOG)
Ph. Balbiani, L. Fariñas del Cerro, A. Herzig (1988), Declarative sematics for modal logic programs.
Proc. Int. Conf. on Fifth Generation Computer Systems (FGCS-88).
(definition of a declarative semantics for MOLOG)
Get abstract
Ph. Balbiani, A. Herzig, M. Lima Marques (1991), TIM: the Toulouse Inference Machine for non-classical logic programming.
Proc. Int. Workshop on Processing Declarative Knowledge (PDK-91), Springer Verlag, LNAI 567.
(definition of a large class of metainterpreters supported by MOLOG)
Get abstract
J.-M. Alliot, A. Herzig, M. Lima Marques (1992), Implementing Prolog extensions: a parallel inference machine.
Proc. Int. Conf. on Fifth Generation Computer Systems (FGCS-92).
(description of an abstract inference engine for MOLOG)
Get abstract - Get PostScript - Get PostScript, gzipped
L. Fariñas del Cerro, A. Herzig (1993), Metaprogramming through intensional deduction: some examples.
Proc. Third Workshop on Metaprogramming in Logic (META-92), Springer Verlag, LNCS 649.
(overview of non-classical logic programming in MOLOG)

Description of the package

The MOLOG implementation that is described here is a metainterpreter written in C-Prolog.

The heart of the interpreter

The 6 following files contain the C_Prolog 1.6 version 1.02 of the MOLOG interpreter:

ini: Initialization of the environment
m_top_level: top level loop
m_translate: syntactical analysis
m_treat: action handler
m_utilities: utilitaries predicates
m_predefined: Molog-Prolog interface
C_Prolog,
Quintus_Sicstus, and
SWI_Prolog: Compatibility files for various versions of Prolog, renaming built-in predicates.
Quintus_not: compatibility file defining predicate `not' for Quintus_Prolog.

The rule files

The following files contain resolution rules for several modal systems. In particular file epi_fool is for modal logic S4, file mod_c_ext

is for contextual logic programming, and file np_hyp

is for N_Prolog.

classical: resolution rules for classical first-order logic
epi_fool: resolution rules for modal logic S4 (supporting as well multi-modal versions of S4 and the fool operator of epistemic logic)
hyp: resolution rules for hypothetical reasoning.
hyp_0: resolution rules for hypothetical reasoning. Each clause must be used exactly once.
hyp_mn: resolution rules for hypothetical reasoning. Each clause must be used at least once.
hyp_pl: resolution rules for hypothetical reasoning. Each clause may be used only once.
hyp_sans: resolution rules for hypothetical reasoning, with specification of predicates not to be used (introduced by \).
mod_c_ext: resolution rules for Monteiro and Porto's contextual logic programming (an extension of Prolog with modules).
mod_exp: resolution rules for modules with predicate export.
mod_fus: resolution rules for modules. Every module listed in the goal may be used.
mpli_op: hypothetical reasoning with two implication symbols. <-- introduces goals, and <== introduces hypotheses that may be used in order to solve a goal.
np_hyp: resolution rules for Gabbay and Reyle's N_Prolog (an extension of Prolog with hypothetical goals which corresponds to the positive fragment of intuitionistic logic)
np_sans: resolution rules for N_Prolog based on hypothetical reasoning, with specification of predicates not to be used.
pl_sans: resolution rules for hypothetical reasoning, with specification of predicates not to be used, each clause may be used only once.

Note: A XXX.rule file is a compiled file corresponding to the resolution rule file called XXX.

Fact files

The following files are test databases (fact files):

fib: computation of Fibonacci numbers (to be used with mpli_op).
rha: examples for classical, N_Prolog and hypothetical reasoning (mpli).
rha_mod: examples for modules
test_sans: examples for hypothetical reasoning with specification of predicates not to be used ("_sans" rule files).

The last file is a MOLOG database that describes the well-known wise men puzzle.

wise_men: commented database
wise_trie: file containing the full set of clauses in optimized order

Note: A XXX.mol file is a compiled file corresponding to the fact file called XXX.

Some remarks about portability

Though C_Prolog is claimed to be fully Edinburgh Prolog compatible, some problems appeared when we tried to use UNH Prolog. Predefined operators have not the same precedence number. The operators are defined in the file m_top_level :

MOLOG operators         Prolog predefined operators

op(1200,fy,?).
op(1200,fy,@).
                        op(1000,xfy,,).
                        ...
                        ...
                        ...
                        op(300,xfx,mod)
op(150,xfy,<--).
op(100,xfy,&).
op(50,xfy,':').

In C_Prolog 1.5 and DEC_10 Prolog the precedences of the predefined operators range between 1000 (operator `,') and 300 (operator mod). The precedence of `?' and `@' must be greater than that of `,', and the precedence of ` <--' must be less than that of the 'mod' operator.

The interpreter currently runs on C-Prolog, Quintus-Prolog, Sicstus-Prolog, and SWI-Prolog.

How to use MOLOG

Once the user has chosen the set of inference rules to be used (and thus a non-classical logic), MOLOG works just as a Prolog interpreter: given a database DB and a goal G, the interpreter answers yes if DB implies G in that non-classical logic. New database clauses can be asserted with @: @p. adds p to the current database.

In the following we explain how to use MOLOG by an example, namely the famous wise men puzzle. The puzzle and its axiomatization are described in the wise_men file. The epistemic logic it uses is multimodal S4 together with a fool agent (who knows something if everybody knows it). The corresponding inference rules are in the file epi_fool.rule.

Call the PROLOG interpreter.
Consult the file containing the initialization procedure.
?- [ini].
Call the MOLOG interpreter.
?- molog. ** Welcome on MOLOG (the C_prolog version 1.02) ** Please give the name of the rule file you want to use:
We choose the epi_fool logic.
epi_fool. epi_fool.rule reconsulted
We consult the wise_men file.
U> ld_fact(wise_men). wise_men.mol consulted yes
The trace mode is off, if you want to set it on
U> tron. yes
We now want to know whether s3 knows that p3. For skolemization matters, the goal must first be translated (see below for a description of the translation):
comi(s3,2):p3. yes
We quit the interpreter.
U> stop. **** Goodbye, MOLOG halted ****

A fact p can be asserted by asking the goal ``@p.''.

Compiled rule files and fact files are not provided. The Molog predicate COMPI_RULES (resp. COMPI) may be used to compile resolution rule files (resp. fact files), producing ".rule" (resp ".mol") files. COMPI_RULES must be used in Ruler mode (type "ruler" instead of the name of a rule file) or under PROLOG after loading MOLOG.

Note: SWI-Prolog doesn't accept files compiled using other Prolog interpreters.

Algorithm for the translation of S4 Horn clauses :

There are two functions T and TG, the second one being for the translation of goal clauses.

If p is a predicate then T(p) = p, and TG(p) = p.
T(A <-- B) = (T(A) <-- TG(B))
TG(A & B) = (TG(A) & TG(B))
T(nec(X):A) = nec(X):T(A)
T(pos(X):A) = posi(X,i):T(A) (i must be unique )
TG(nec(X):A) = posi(X,i):T(A)
TG(pos(X):A) = pos(X):A

E.g.

T(pos(X):p <-- nec(X):q & pos(X):r) 

         = pos(X,i):p <-- posi(X,i):q & pos(X):r)

Andreas.Herzig@irit.fr / http://www.irit.fr/~Andreas.Herzig