https://github.com/theoremprover-museum/CLIN
Tip revision: e7082fbde3634286f458d64846699ae488fe18f3 authored by Michael Kohlhase on 22 December 2016, 09:28:55 UTC
initial commit, thanks to David Plaisted
initial commit, thanks to David Plaisted
Tip revision: e7082fb
prover
%%% Clause-Linking Prover
%%% (CLIN)
%%%
%%% DAVID A. PLAISTED and SHIE-JUE LEE
%%% Department of Computer Science
%%% University of North Carolina
%%% Chapel Hill, NC 27599--3175
%%% (919) 962-{1751|1934}
%%% {plaisted|lee}@cs.unc.edu
%%%
%%% version 1.0
%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% ALS Prolog Version %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%
% :- [-'ALS'].
%%%%%%%%%%%%%%%%%%%%%%%
%%% CProlog Version %%%
%%%%%%%%%%%%%%%%%%%%%%%
% :- [-'Cprolog'].
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Eclipse Prolog Version %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- compile('Eclipse').
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Quintus Prolog Version %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% :- compile('Quintus').
%%% Consult files.
:- load_file('auxiliary').
:- load_file('clausify').
:- load_file('command').
:- load_file('exprules').
:- load_file('fls').
:- load_file('hyper').
:- load_file('instdel').
:- load_file('interp').
:- load_file('skolem').
:- load_file('define').
:- load_file('library').
:- load_file('main').
:- load_file('pc').
:- load_file('replace').
:- load_file('simplify').
:- load_file('spc').
:- load_file('try').
:- load_file('xvisor').
%%% Initialization
:- abolish(clin_version,1).
:- assert(clin_version('1.0')).
%%% Welcome message.
:- (clin_version(Version),
nl, tab(15),write('WELCOME TO CLIN '),
version(Version),write(Version),nl,nl,nl).
helpmsg :-
nl,write_line(2,'USER GUIDE : '),
write_line(2,'Key in "prove(File).".'),
write_line(2,'Key in "settings." to list all current settings.'),
write_line(2,'For more info., type "choice.".'),
write_line(2,'These info. can be reviewed by typing in "helpmsg.".'),
nl.
:- helpmsg.