1%
    2%  twb_vpdl.pl:  interface to our VPDL prover built using Tableaux Workbench
    3%
    4%  Copyright 2008, Ryan Kelly
    5%
    6%  The main predicate we export is entails/2, which shells out to a stand-alone
    7%  prover for "PDL-plus-variable-assignment".
    8%
    9
   10twb_pdl_exe('vpdl/vpdl.twb').
   11
   12entails(Axs,Conc) :-
   13    maplist(copy_term,Axs,Axs2),
   14    copy_term(Conc,Conc2),
   15    twb_pdl_prove(Axs2,Conc2,yes).
   16
   17twb_pdl_prove(Axioms,Conc,Result) :-
   18    % Create input/output files
   19    tmp_file(twb_in,InFile),
   20    tmp_file(twb_out,OutFile),
   21    tell(InFile),
   22    % Universally quantify all free variables in conc
   23    free_vars(Conc,ConcVars),
   24    ( ConcVars = [] ->
   25          Conc2 = Conc
   26    ;
   27          guess_var_types(ConcVars,Conc,TypedVars),
   28          Conc2 = !(TypedVars : Conc)
   29    ),
   30    % Write out (Axioms) -> (Conjecture)
   31    write('('),
   32    twb_write_axioms(Axioms), !,
   33    write(') -> ('),
   34    twb_write(Conc2), write(').'), nl,
   35    told, !,
   36    % Call TWB and have it write its conclusions into output file
   37    twb_pdl_exe(CmdFile),
   38    sformat(PCmd,'~w < ~w > ~w 2>&1',[CmdFile,InFile,OutFile]),
   39    shell(PCmd,_),
   40    % Grep output file for "Result:Closed" indicating truthity
   41    sformat(TCmd,'grep "Result:Closed" ~w > /dev/null',[OutFile]),
   42    ( shell(TCmd,0) ->
   43        Result = yes
   44    ;
   45        % Check for any fatal errors, and report them
   46        sformat(ErrCmd,'grep "Fatal" ~w > /dev/null',[OutFile]),
   47        ( shell(ErrCmd,0) ->
   48            throw(badly_formed_twb_file(InFile))
   49        ;
   50            % Propositional prover, so we cannot get Result=unknown
   51            Result = no
   52        )
   53    ).
   54
   55
   56%
   57%  twb_write(P)  -  write formula in TWB PDL format
   58%
   59
   60twb_write(P) :-
   61    twb_write_fml(P), !.
   62
   63twb_write_fml(true) :-
   64    write(' (Verum) '), !.
   65twb_write_fml(false) :-
   66    write(' (Falsum) '), !.
   67twb_write_fml(A=B) :-
   68    write('( '),
   69    twb_write_term(A),
   70    write(' == '),
   71    twb_write_term(B),
   72    write(' )'), !.
   73twb_write_fml(A\=B) :-
   74    write('~ ( '),
   75    twb_write_term(A),
   76    write(' == '),
   77    twb_write_term(B),
   78    write(' )'), !.
   79twb_write_fml(P) :-
   80    is_atom(P),
   81    twb_write_pred(P).
   82twb_write_fml(P & Q) :-
   83    write('('),
   84    twb_write_fml(P),
   85    write(' & '),
   86    twb_write_fml(Q),
   87    write(')').
   88twb_write_fml(P | Q) :-
   89    write('('),
   90    twb_write_fml(P),
   91    write(' v '),
   92    twb_write_fml(Q),
   93    write(')').
   94twb_write_fml(P => Q) :-
   95    write('('),
   96    twb_write_fml(P),
   97    write(' -> '),
   98    twb_write_fml(Q),
   99    write(')').
  100twb_write_fml(P <=> Q) :-
  101    write('('),
  102    twb_write_fml(P),
  103    write(' <-> '),
  104    twb_write_fml(Q),
  105    write(')').
  106twb_write_fml(~P) :-
  107    write('~ ('),
  108    twb_write_fml(P),
  109    write(')').
  110twb_write_fml(!([]:P)) :-
  111    twb_write_fml(P).
  112twb_write_fml(!([V:T|Vs]:P)) :-
  113    write('( '),
  114    twb_write_fml_sols(twb_valuate_var(T,!(Vs:P)),V,'&',true),
  115    write(' )'), flush.
  116twb_write_fml(?([]:P)) :-
  117    twb_write_fml(P).
  118twb_write_fml(?([V:T|Vs]:P)) :-
  119    write('( '),
  120    twb_write_fml_sols(twb_valuate_var(T,?(Vs:P)),V,'v',false),
  121    write(' )'), flush.
  122twb_write_fml(knows(A,P)) :-
  123    write('( ['),
  124    write(A),
  125    write('] ('),
  126    twb_write_fml(P),
  127    write('))').
  128twb_write_fml(pknows0(E,P)) :-
  129    epath_vars(E,Vars),
  130    epath_enum_vars(E,En1),
  131    epath_elim_impossible_branches(En1,[],En),
  132    ( En = (?false) ->
  133        write(' (Verum) ')
  134    ; En = (?true) ->
  135        twb_write_fml(P)
  136    ;
  137        write('( ['),
  138        number_vars(Vars),
  139        twb_write_path(En),
  140        write('] ('),
  141        twb_write_fml(P),
  142        write('))')
  143    ).
  144
  145
  146twb_valuate_var(T,Fml,V,Res) :-
  147    call(T,Val), subs(V,Val,Fml,Res1),
  148    copy_fml(Res1,Res2),
  149    simplify(Res2,Res).
  150
  151twb_write_fml_sols(Pred,Var,Sep,_) :-
  152    call(Pred,Var,Sol),
  153    twb_write_fml(Sol),
  154    write(' '), write(Sep), write(' '), fail.
  155twb_write_fml_sols(_,_,_,Final) :-
  156    twb_write_fml(Final).
  157
  158twb_write_terms([],_).
  159twb_write_terms([T],_) :-
  160    twb_write_term(T), !.
  161twb_write_terms([T,T2|Ts],Sep) :-
  162    twb_write_term(T),
  163    write(Sep),
  164    twb_write_terms([T2|Ts],Sep).
  165
  166twb_write_term(T) :-
  167    T =.. [F|Args],
  168    ( length(Args,0) ->
  169      write(F)
  170    ;
  171      write(F), write('_'),
  172      twb_write_terms(Args,'_')
  173    ).
  174    
  175twb_write_pred(P) :-
  176    P =.. [F|Terms],
  177    write(F),
  178    (Terms \= [] -> write('__'), twb_write_terms(Terms,'__') ; true).
  179
  180twb_write_axioms([]) :-
  181    write('Verum').
  182twb_write_axioms([A]) :-
  183    twb_write_fml(A).
  184twb_write_axioms([A|Axs]) :-
  185    twb_write_fml(A), write(' & '),
  186    twb_write_axioms(Axs).
  187
  188
  189twb_write_path(E1 ; E2) :-
  190    write('('),
  191    twb_write_path(E1),
  192    write(' ; '),
  193    twb_write_path(E2),
  194    write(')').
  195twb_write_path(E1 | E2) :-
  196    write('('),
  197    twb_write_path(E1),
  198    write(' U '),
  199    twb_write_path(E2),
  200    write(')').
  201twb_write_path(?(P)) :-
  202    write('( ? '),
  203    twb_write_fml(P),
  204    write(' )').
  205twb_write_path(E*) :-
  206    write('( * '),
  207    twb_write_path(E),
  208    write(' )').
  209twb_write_path(-VA) :-
  210    ( VA = [] ->
  211      twb_write_path(?true)
  212    ;
  213      write('( '),
  214      twb_write_vassign(VA),
  215      write(' )')
  216    ).
  217twb_write_path(A) :-
  218    agent(A),
  219    write(A).
  220
  221twb_write_vassign([]).
  222twb_write_vassign([(X:V)|Xs]) :-
  223    write('! '), write(X), write(' <= '), twb_write_term(V), write(' '),
  224    twb_write_vassign(Xs)