home *** CD-ROM | disk | FTP | other *** search
/ ftp.cs.yorku.ca 2015 / ftp.cs.yorku.ca.tar / ftp.cs.yorku.ca / pub / peter / SVT / prover.prolog < prev    next >
Text File  |  2000-01-24  |  3KB  |  91 lines
  1. /*
  2.  
  3.   PROVER
  4.  
  5.   copyright 1992, 1997, P. H. Roosen-Runge
  6.  
  7. A combination of wang and simplify. Loads the theory modules arithmetic.simp
  8. and equality.simp.
  9. %=====================================================
  10. % Ver. 1.0 July 8, 1992.  Based on Ver 1.4.1 of simplify.
  11. %      1.1 July 12: incorporates use of equalities to eliminate variables,
  12. %                   using equtaut.pl.
  13. %      1.2 July 14: retries simplified sequent as long as simplification
  14. %                   produced new result.
  15. %      1.3 April 21, 1997: loads theory files on activation to allow 
  16.                      user-supplied files
  17. %      1.4.2 December 23, 1998: consults getTheories.prolog
  18. %      1.4.3 December 29: uses theory/1 predicate from getTheories
  19. %      1.4.4 Feb. 26, 1999: re-compiled with getTheories v1.1,
  20. %               to avoid crash if theory file missing.
  21. %               error/1 added.
  22. %      1.4.5 March 14: re-compiled with output.prolog v2.3.1,
  23. %               to avoid non-deterministic indenting.
  24. %               and simp.prolog v 1.9.1 to repair prove(P).
  25. %      1.4.6 December 13: re-compiled with equtaut v. 1.3
  26. %==================================================================
  27. */
  28.  
  29. :- no_style_check(single_var).
  30. :- multifile '->>'/2. :- dynamic '->>'/2.
  31.  
  32. :-ensure_loaded([library(basics), library(arg), library(change_arg),
  33.       library(occurs)]).
  34.  
  35. % assumes library path defined in prolog.ini
  36. :- ensure_loaded([lib('simp.prolog'),
  37.                  lib('equtaut.prolog')]).
  38.  
  39. user_error_handler(_,_,_,_) :-
  40.         write('!! Something wrong.'), nl, halt.
  41. error(X) :- write('!! '), write(X), nl. 
  42.  
  43. activate :- 
  44.   write('Version 1.4.6, December 13, 1999.'), 
  45.         nl,
  46.         getTheories,
  47.     proveTerms
  48.      ;
  49.     nl, write('!! Something wrong.'), nl, halt.
  50.  
  51. proveTerms :- read(T),
  52.        (  T==end_of_file -> halt
  53.     ;
  54.      ( T=theory(File) -> theory(File)
  55.         ;
  56.            T=assert((Rule)) -> asserta((Rule))
  57.       ;
  58.        write(T), nl, try(T), nl
  59.      ),
  60.       proveTerms
  61.          
  62.        ).
  63.  
  64. try(T) :- 
  65.     simplify(T,S), !,  
  66.     (tautology(S) -> nl, write('* Valid.'),nl
  67.          ;
  68.         nl, write('* Cannot prove '), write(S), write('.'), nl
  69.         ).
  70.  
  71. /* tautology/2 missing
  72. try(T) :- tautology(T, Seq), write('* Valid.'), nl
  73.          ;
  74.       makeProp(Seq, Prop), simplify(Prop, SimpProp),
  75.       (Prop = SimpProp -> 
  76.           write('Cannot prove '), write(SimpProp), write('.')
  77.       ;
  78.        try(SimpProp)
  79.           ).
  80.  
  81. makeProp(L >> R, LP implies RP) :-
  82.     makeProp(left, L, LP), makeProp(right, R, RP).
  83.  
  84. makeProp(left, [], true).
  85. makeProp(right, [], false).
  86. makeProp(_, [T], T).
  87. makeProp(left, [T | Rest], T and P) :- makeProp(left, Rest, P).
  88. makeProp(right, [T | Rest], T or P) :- makeProp(right, Rest, P). 
  89. */         
  90. :- save_program(prover, activate).
  91.