MVL theorem proving system available via anonymous ftp

Matthew L. Ginsberg <>
Date: Tue, 27 Nov 90 10:22:40 PST
From: Matthew L. Ginsberg <>
Message-id: <9011271822.AA00410@t.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  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