MVL theorem proving system available via anonymous ftp

• Mail folder: Interlingua Mail
• Next message: Richard Fikes: "Interlingua Nonmon Proposal and Meeting Agenda Items"
• Previous message: Richard Fikes: "A CLASSIC to KIF Exercise"

Date: Tue, 27 Nov 90 10:22:40 PST
From: Matthew L. Ginsberg <ginsberg@t.stanford.edu>
Message-id: <9011271822.AA00410@t.Stanford.EDU>
To: interlingua@venera.isi.edu, kif@cs.stanford.edu
Subject: MVL theorem proving system available via anonymous ftp

To help further the interlingua discussion, I've made my theorem prover,
MVL, available via anonymous ftp from t.stanford.edu.  When you connect,
enter "ftp" as your user name, and then anything you want as a password.
Do a cd to mvl and then an mget *.  There is a README file included.

MVL does not purport to be an interlingua, but it probably has features
that an interlingua should share.  It is a "flexible" theorem prover, in that
the user can specify the logic he wants to use -- first-order, ATMS, default
reasoning, circumscription, probabilistic, or one he invents himself.  The
knowledge is stored in a *somewhat* uniform way (ie, the language is uniform
but the truth values are not); the real value of the system is that it
includes inference tools that work with any of these reasoning methods.
(Inference not being part of the interlingua, but MVL is supposed to be
a theorem prover, not an interlingua.)

Documentation and installation instructions are also included.

						Matt Ginsberg