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 >
Wrap
Text File
|
2000-01-24
|
3KB
|
91 lines
/*
PROVER
copyright 1992, 1997, P. H. Roosen-Runge
A combination of wang and simplify. Loads the theory modules arithmetic.simp
and equality.simp.
%=====================================================
% Ver. 1.0 July 8, 1992. Based on Ver 1.4.1 of simplify.
% 1.1 July 12: incorporates use of equalities to eliminate variables,
% using equtaut.pl.
% 1.2 July 14: retries simplified sequent as long as simplification
% produced new result.
% 1.3 April 21, 1997: loads theory files on activation to allow
user-supplied files
% 1.4.2 December 23, 1998: consults getTheories.prolog
% 1.4.3 December 29: uses theory/1 predicate from getTheories
% 1.4.4 Feb. 26, 1999: re-compiled with getTheories v1.1,
% to avoid crash if theory file missing.
% error/1 added.
% 1.4.5 March 14: re-compiled with output.prolog v2.3.1,
% to avoid non-deterministic indenting.
% and simp.prolog v 1.9.1 to repair prove(P).
% 1.4.6 December 13: re-compiled with equtaut v. 1.3
%==================================================================
*/
:- no_style_check(single_var).
:- multifile '->>'/2. :- dynamic '->>'/2.
:-ensure_loaded([library(basics), library(arg), library(change_arg),
library(occurs)]).
% assumes library path defined in prolog.ini
:- ensure_loaded([lib('simp.prolog'),
lib('equtaut.prolog')]).
user_error_handler(_,_,_,_) :-
write('!! Something wrong.'), nl, halt.
error(X) :- write('!! '), write(X), nl.
activate :-
write('Version 1.4.6, December 13, 1999.'),
nl,
getTheories,
proveTerms
;
nl, write('!! Something wrong.'), nl, halt.
proveTerms :- read(T),
( T==end_of_file -> halt
;
( T=theory(File) -> theory(File)
;
T=assert((Rule)) -> asserta((Rule))
;
write(T), nl, try(T), nl
),
proveTerms
).
try(T) :-
simplify(T,S), !,
(tautology(S) -> nl, write('* Valid.'),nl
;
nl, write('* Cannot prove '), write(S), write('.'), nl
).
/* tautology/2 missing
try(T) :- tautology(T, Seq), write('* Valid.'), nl
;
makeProp(Seq, Prop), simplify(Prop, SimpProp),
(Prop = SimpProp ->
write('Cannot prove '), write(SimpProp), write('.')
;
try(SimpProp)
).
makeProp(L >> R, LP implies RP) :-
makeProp(left, L, LP), makeProp(right, R, RP).
makeProp(left, [], true).
makeProp(right, [], false).
makeProp(_, [T], T).
makeProp(left, [T | Rest], T and P) :- makeProp(left, Rest, P).
makeProp(right, [T | Rest], T or P) :- makeProp(right, Rest, P).
*/
:- save_program(prover, activate).