\documentstyle[a4]{article}

\begin{document}


Sum\'ario sobre {\sl Sistemas Gen\'ericos de Prova Autom\'atica de Teoremas}

\begin{description}
\item[MVL (Multi-Valued Logic)] {\ } \\
\begin{itemize}
\item
  MVL (Multi-Valued Logic) is a theorem proving system written in Common
   Lisp. MVL is a bilattice-based reasoning system.  By changing the
   bilattice, you can use MVL to do truth maintenance, nonmonotonic
   reasoning, first-order reasoning, and a variety of other reasoning
   strategies.  
\item
  MVL is available by anonymous ftp from t.stanford.edu in
  /mvl/mvl.tar.Z. A user's manual may be found in /mvl/manual.tex. For
  more information, contact Matthew L. Ginsberg, $<$ginsberg\@t.stanford.edu$>$
  or $<$ginsberg@cs.stanford.edu$>$. Matthew asks that you send him an email
   message if you retrieve the system by anonymous ftp.
\end{itemize}
\item[Boyer-Moore] {\ } \\
\begin{itemize}
\item 
  ???
\item
\begin{verbatim}
   ftp.cli.com:pub/nqthm/nqthm.tar.Z   Contact: kaufman@cli.com
   rascal.ics.utexas.edu:/pub/             128.83.138.20
      nqthm/               Boyer and Moore's theorem prover.
                           Also available from ftp.cli.com:/pub/nqthm.
      proof-checker/       Matt Kaufmann's proof checking
                           enhancements to nqthm.
   The mailing list nqthm-users-request@cli.com is for users of the
   Boyer-Moore theorem-prover, NQTHM.
\end{verbatim}
\end{itemize}

\item[DTP] {\ } \\
\begin{itemize}
\item
  DTP is a general theorem prover incorporating domain-independent control
   of inference.  Implemented in CLtL2 Common Lisp, it runs in Franz
   Allegro, Lucid, and Macintosh (MCL) Common Lisp.  
\item
  It is available by
   anonymous ftp from meta.stanford.edu:pub/dtp/ [36.8.0.54].  Contact
   Don Geddis $<$Geddis@CS.Stanford.EDU$>$ for more information.
\end{itemize}

\item[RRL (Rewrite Rule Laboratory)] {\ } \\
\begin{itemize}
\item 
  ???
\item herky.cs.uiowa.edu:public/rrl \qquad   [128.255.28.100]
\end{itemize}

\item[FRAPPS (Framework for Resolution-based Automated Proof Procedures)] {\ } \\
\begin{itemize}
\item
  FRAPPS (Framework for Resolution-based Automated Proof Procedures) is
   a portable resolution theorem-prover written in Common Lisp. 
\item
  It is
   available via anonymous ftp from a.cs.uiuc.edu:/pub/frapps [128.174.252.1].
   If you take a copy of FRAPPS, please send a short note to Prof.
   Alan M. Frisch $<$frisch@cs.uiuc.edu$>$.
\end{itemize}

\item[PROOFCHK] 
  For use with the Shaum's \_Outline of Logic\_, natural deduction.
   Student enters proof and the theorem prover (a help button) offers 
   graded series of hints for solutions. Also includes a validity 
   checker and help screens.

\begin{verbatim}
       Send a disk and self- addressed stamped mailer to:
       John Nolt
       Philosophy Department
       University of Tennessee
       Knoxville, TN 37996-0480
\end{verbatim}

\item[Nqthm] 
  Boyer- Moore theorem prover (see book by same authors). 
   Rascal.ics.utexas.edu :/pub/nqthm  

\item[Otter]  
  Theorem Prover
   Used with \_Automated Reasoning: Introduction and Applications\_,
   Larry Wos et al, McGraw-Hill 1992.
   Herky.cs.uiowa.edu :/public/otter
 
\item[DTP] meta.stanford.edu :/pub/dtp  

\item[Setheo (SEquential THEOrem prover)]

  Sun Sparcstations and X Windows.
   flop.informatik.tu-muenchen.de (131.159.8.35) :/pub/fki
   email: setheo@informatik.tu-muenchen.de

\item[HOL (Higher Order Logic)]
  Used with \_Introduction to HOL: A Theorem Proving Environment for
   Higher Order Logic\_. Ed. M.J.C. Gordon and T.F. Melham, Cambridge 
   University Press 1993
   ftp.cs.tut.fi :/pub/src/DisCo/hol90.6    

\item[ MacLL] 
   "MacLogic-like proof editor for linear logic", by Roy Dyckhoff
    and the MALT (Machine Assisted Logic Teaching) project at
    St. Andrew's University.
    138.251.192.40 (tamdhu.dcs.st-and.ac.au) :/pub/malt/macLL. Also
    get MacLogic fonts from /pub/malt/maclogic.


 \item[ Coq] 
  "Implementation of the Calculus of Inductive Constructions, a powerful 
   logic accepting higher-order reasoning and definition of a 
   wide class of functions. It also allows the extraction of proven-
   correct ML programs from proofs. It is implemented in caml-light 
   (ML dialect) and thus runs on unix machines, macintosh's and PC's." 
   ftp.inria.fr :/INRIA/coq.  
   email address: coq@margaux.inria.fr.
   
 \item[Isabelle]
   General theorem prover, many-sorted first-order logic, constructive 
    and classical versions higher-order logic, Zermelo-Fraenkel set theory,
    an extensional version of Martin-L\"of's Type Theory, the classical 
    first-order sequent calculus LK, the modal logics T, S4, and S5, 
    the Logic for Computable Functions, LCF, the Lambda Cube.
    ftp.cl.cam.ac.uk [128.232.0.56] :/ml/Isabelle93.tar.gz
    email: Larry.Paulson@cl.cam.ac.uk (Lawrence Paulson)

  \item[LCF (Logic for Conputable Functions)] 
    Interactive theorem prover. Proofs conducted in PPLAMBDA,
    a natural deduction logic based on the domain theory of Dana Scott,
    and is particularly suitable for proofs involving denotational 
    semantics, lazy evaluation, or higher-order functions.
    LCF provides a metalanguage (Standard ML), a functional programming 
    language whose values include PPLAMBDA terms, formulas, and theorems.
    Theorem-proving primitives such as inference rules, subgoaling 
    strategies (tactics), and simplifiers are implemented as ML functions.
    The user can extend LCF by programming in ML.
    ftp.cl.cam.ac.uk :/ml

  \item[ Mizar MSE] 
    first order Multi- Sorted predicate calculus with Equality
    Logic validity and proof checking, mathematical proofs. 
    menaik.cs.ualberta.ca (129.128.4.241) :/pub/Mizar-MSE
    email: piotr@cs.ualberta.ca (Piotr Rudnicki)

  \item[Nuprl3] 
    Proof development system described in \_Implementing Mathematics\_,
    Prentice-Hall, 1986. Nuprl4 scheduled for released late August  
    1994.
    ftp.cs.cornell.edu  :/pub/n/nuprl-3-2.tar.Z
                        :/pub/nuprl   (docs)
    email: kate@cs.cornell.edu (Prof. Constable)

\end{description}

\end{document}
