------------------------------------------------------------
PROTEIN - A PROver with a Theory Extension INterface
------------------------------------------------------------

What PROTEIN is:

PROTEIN  is  an  automated  theorem prover  for  first-order
clause  logic.   It  follows  Loveland's  Model  Elimination
procedure   and  is  implemented   according  to   Stickel's
PTTP-Technique,  i.e.  the  input specification  is compiled
into a Prolog program.  Besides "Model Elimination", PROTEIN
features  various versions  of  "Restart Model Elimination".
Furthermore,  PROTEIN has  an interface for including theory
knowledge  into the proving process.  Another feature is the
computation of the negation of a literal  according to WGCWA
or GCWA.

------------------------------------------------------------

Machine and Software Requirements:

PROTEIN is written in ECRC's Prolog-dialect ECLiPSe.

	http://www.ecrc.de/eclipse/eclipse.html

------------------------------------------------------------

Installation:

- untar and unzip the pakage !
  You get  the sources,  some  sample problems  in directory
  SAMPLES, the documentation protein.ps, and an PROTEIN-mode
  for Emacs in protein.el.
- Set  the global variable  $PROTEINHEADER  to the directory
  containing  the files t_header*.pl  and  set  the variable
  $HYPERHOME  to  the directory  containing  Michael Kuehn's
  prover Hyper,hyper!  (This Prover  is  optionally used for
  consistency test  while computing the general closed world
  assumption)
- Read the documentation  !
  Section 3.2 "Invoking" tells you how to invoke PROTEIN and
  how to make an executable.
- If you want to use  one of the treeviewers xptree or tview
  which are not part of the PROTEIN package,  Section 3.2 of
  the documentation tells you how to make the executables of
  the   tools   protein2xptree  and   protein2tview,   which 
  translate  the tree  generated by PROTEIN  in a syntax for
  the treeviewers.
- Include  the directory  with the executable in your path !

------------------------------------------------------------

Adresses:

Bug Report:
  peter@informatik.uni-koblenz.de and
  doro@informatik.uni-koblenz.de

PROTEIN home page: 
  http://www.uni-koblenz.de/ag-ki/Implementierungen/Protein/