Porting to other Prolog Systems:

• 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:

• 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,_,_)).
    

    to

    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@ira.uka.de
  $Id: leantap_prologs.html,v 1.1 2012/11/15 00:14:20 beckert Exp $