1%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    2%
    3% Copyright 2003-2010, Renate Schmidt,  University of Manchester
    4%           2009-2010, Ullrich Hustadt, University of Liverpool
    5%
    6%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    7%
    8% Main file for loading the source files of a PDL tableau prover
    9%
   10% Ways of running the prover from the command line:
   11%
   12%     1. Basic
   13%        pl -f pdl_tableau.pl 
   14%        pl -f pdl_tableau.pl -g "provable(and(dia(comp(b,star(a)),p), box(comp(star(b),star(a)), not(p))), Result)." -t halt
   15%        pl -f pdl_tableau.pl -g "satisfiable(and(dia(comp(b,star(a)),p), box(comp(star(b),star(a)), not(p))), Result)." -t halt
   16%
   17%     2. Testing for verification purposes on a collection of problems
   18%        pl -f pdl_tableau.pl -g "problem(51, satisfiable, Result)." -t halt
   19%        pl -f pdl_tableau.pl -g 'testing(routine)' -t halt
   20%        (`routine' refers to the routine problems in the problem list.)
   21%        pl -f pdl_tableau.pl -g "load_calculus(pdl_dGM_nd), testing(routine)." -t halt > & /dev/null
   22%
   23%     3. Enable/Disable output of derivations
   24%        By default, this version of pdl-tableau disables most output by
   25%        loading 'no_output.pl', see 'ensure_loaded([...])' below
   26%        To enable output, one has to load 'output.pl' instead of 'no_output.pl'.
   27%        Furthermore, the set_output_format predicate at the end of this file
   28%        determines the output format that is used in the file /tmp/search.log
   29%        By default it is set to 'none', but can be changed to 'txt', for plain
   30%        text output, and 'latex', for latex output.
   31%
   32% For further configuration option see the comments on the calculus variations
   33% below.
   34
   35
   36%       
   37%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   38%
   39% Basic source files
   40
   41:- ensure_loaded([
   42       normalise,
   43       prover,
   44       caching,
   45       problems,
   46       testing,
   47       settings,
   48       no_output
   49   ]).   50
   51:- dynamic inconsistent/1.   52:- dynamic consistent/3.   53
   54%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   55%
   56% Calculus (first the rule, then the corresponding file)
   57
   58% Uses
   59%       X_{<a*>p}
   60%   (X)-----------
   61%       p | <a>X
   62%
   63%         F v G
   64%   (v) -------------
   65%         F | G
   66%
   67%:- load_calculus(pdl_dGM_nd).
   68% 'nd' is short for `not disjoint' branches
   69
   70% Uses
   71%       X_{<a*>p}
   72%   (X)-----------
   73%       p | <a>X
   74%
   75%         F v G
   76%   (v) -------------
   77%         F | -F, G
   78%
   79%:- load_calculus(pdl_dGM_bcs).
   80% 'bcs' is short for `boolean complement splitting'
   81
   82
   83% Uses
   84%        X_{<a*>p}
   85%   (X)--------------
   86%       p | -p, <a>X
   87%
   88%         F v G
   89%   (v) -------------
   90%         F | G
   91%
   92:- load_calculus(pdl_dGM).   93
   94% Uses
   95%        X_{<a*>p}
   96%   (X)--------------
   97%       p | -p, <a>X
   98%
   99%         F v G
  100%   (v) -------------
  101%         F | -F, G
  102%
  103%:- load_calculus(pdl_dGM_fcs).
  104% 'fcs' is short for 'full complement splitting'
  105
  106
  107%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  108%
  109% Inference closure rules (first the rule, then the corresponding file)
  110%
  111
  112% Uses
  113%
  114%   p, -p
  115%   ----- (p must be atomic and X-free)
  116%   clash
  117%
  118%:- use_module(inf_closure_atomic).
  119
  120% Uses
  121%
  122%   F, -F
  123%   ----- (F must be X-free)
  124%   clash
  125%
  126%:- use_module(inf_closure_strict).
  127
  128% Uses
  129%
  130%   F, -F
  131%   ----- (F must be X-free)
  132%   clash
  133%
  134%   X_{<a*>p}, -<a*>p
  135%   -----------------
  136%        clash
  137%
  138:- use_module(inf_closure_x_free).  139
  140%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  141%
  142% Logical settings
  143
  144%:- set_negate_first(yes).    % negate problem first (does not
  145                              % change the theory)
  146:- set_negate_first(no).  147
  148%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  149%
  150% Miscellaneous settings
  151
  152% Set ouput format for search/proof steps
  153%:- set_output_format(txt).
  154%:- set_output_format(latex).
  155:- set_output_format(none).  156
  157:- set_search_output_filename('/tmp/search.log').  158%:- set_search_output_filename('search.log').
  159:- set_test_output_filename('/tmp/testing.log').  160%:- set_test_output_filename('testing.log').