Porting to other Prolog Systems:

Sicstus Prolog:

lean

runs without changes.

Quintus Prolog:

lean

runs without changes.

SWI-Prolog:

Required changes in leantest.pl, as suggested by M. E. Gegundez Arias (gegundez@mizar.us.es):

the line

:- op(400,fy,-), op(500,xfy,&), op(600,xfy,v),op(650,xfy,=>), op(700,xfy,<=>).

must come after:

:- module(leantest,[provefml/1,incprovefml/1,uv_provefml/1,uv_incprovefml/1]).

Delete the line

 :- use_module(library(lists),[member/2]).

Eclipse:

Required changes, as suggested by Reiner Haehnle (reiner@mail.informatik.kit.edu)

The headers of the source files must be changed for Eclipse; in leantest.pl, it should look like this:

:- module_interface(leantest).
:- op(400,fy,-), op(500,xfy,&), op(600,xfy,v),op(650,xfy,=>), op(700,xfy,<=>).
:- use_module(leantap).
:- use_module(nnf).
:- global provefml/1,incprovefml/1,uv_provefml/1,uv_incprovefml/1.
:- begin_module(leantest).

In leantap.pl it should be

:- module_interface(leantap).
:- export prove/2,prove_uv/2.
:- begin_module(leantap).

and, analogously, for nnf.pl:

:- module_interface(nnf).
:- export nnf/2.
:- begin_module(nnf).

As Eclipse offers sound unification, you can simplify the clauses for prove/5 and prove/7 in leantap.pl as follows:

include the line
```
:- set_flag(occur_check,on).
```
before the definition of prove/5.

symplify the clause for closing a branch in prove/5:

prove(Lit,_,[L|Lits],_,_) :-
        (Lit = -Neg; -Lit = Neg) ->
        (unify(Neg,L); prove(Lit,[],Lits,_,_)).

prove(Lit,_,[L|Lits],_,_) :-
         (Lit = -L ; -Lit = L ; prove(Lit,[],Lits,_,_)).

and the corresponding clause

prove(Lit,_,[L|Lits],_,_,_,_) :-
        (Lit = -Neg; -Lit = Neg ) ->
        (unify(Neg,L); prove(Lit,[],Lits,_,_,_,_)).

in prove/7 to

prove(Lit,_,[L|Lits],_,_,_,_) :-
        Lit = -L; -Lit = L ; prove(Lit,[],Lits,_,_,_,_).

You probably want to include
```
 :- set_flag(debug_compile,off).
```
in leantest.pl, since this speeds up things considerably.

posegga@mail.informatik.kit.edu
$Id: leantap_prologs.html,v 1.1 2012/11/15 00:14:20 beckert Exp $