LILaC
Topic: MOLOG  a tool for nonclassical 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
CProlog
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 metainterpreters.
It is in particular suitable for implementing extensions of
Prolog
with nonclassical 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 multimodal
(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 CProlog, QuintusProlog,
SicstusProlog, and SWIProlog.
Questions and remarks to
Andreas Herzig
 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 KnowledgeBaseed Systems (IPMU86),
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 3550.
(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 (CADE88),
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 (FGCS88).
(definition of a declarative semantics for MOLOG)
Get abstract
 Ph. Balbiani, A. Herzig, M. Lima Marques (1991),
TIM: the Toulouse Inference Machine for nonclassical
logic programming.
Proc. Int. Workshop on Processing Declarative Knowledge (PDK91),
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 (FGCS92).
(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 (META92),
Springer Verlag, LNCS 649.
(overview of nonclassical logic programming in MOLOG)
The MOLOG implementation that is described here is a
metainterpreter written in
CProlog.
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
 MologProlog interface
C_Prolog
,
Quintus_Sicstus
, and
SWI_Prolog
 Compatibility files
for various versions of Prolog,
renaming builtin 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 firstorder logic
epi_fool
 resolution rules for modal
logic S4
(supporting as well multimodal
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
wellknown 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 CProlog, QuintusProlog,
SicstusProlog, and SWIProlog.
Once the user has chosen the set of inference rules to be used
(and thus a nonclassical 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 nonclassical 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: SWIProlog 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 / https://www.irit.fr/~Andreas.Herzig