bedwyr-48x48.png Bedwyr, the not-so-sound logician

v1.4 -- Bedwyr-with-round-tables

  1. what
  2. license
  3. getting
  4. building
  5. documentation
  6. installing
  7. distribution

1. What is Bedwyr?

Bedwyr is a theorem prover for the Level-0/1 fragment of the Linc logic.

It is based on Alwen Tiu's Level-0/1, and Nadathur & Linell's LLambda library, both written in SML. The OCaml translation has been done by Baelde & Ziegler and further development by Baelde & Gacek. It is currently under work by Heath. The system also benefited from the wisdom of Miller, Nadathur and Pientka.

For background on the system, see Mixing Finite Success and Finite Failure in an Automated Prover (Alwen Tiu and Gopalan Nadathur and Dale Miller):


2. License

This is free software, licensed under GPL version 2. A copy of this license can be found in COPYING or, depending on your distribution, /usr/share/common-licenses/GPL-2 or /usr/portage/licenses/GPL-2.

3. Obtaining Bedwyr

Released sources and binaries may be obtained from and packages from

Development sources may be obtained via the commands svn checkout svn:// or svn checkout --username anonsvn (the password is the username).

The project is also available as an opam package, and for Debian ( squeeze main), Gentoo (public user overlay dawan) and Windows. The Linux packages contains the core libraries as well as the complete program.

4. Building Bedwyr

For proper compilation and installation, a Linux environment and the following packages are required:

With the vanilla archive, the single command

$ make

will build bedwyr with default options (no documentation, byte code only). You can customize the process with configure options:

$ autoconf
$ ./configure --no-create [--enable-doc] [--enable-nativecode] [...]
$ make

Use the ./configure --help and make help commands for more details.

Then pick an example in examples/ and run

$ ./bedwyr [-t] examples/<file>.def

or just run

$ ./bedwyr

and type "#help." for a little help.

5. Documentation

Building these files requires the "--enable-doc" configure option (which adds some dependencies on LaTeX, HeVeA, etc), and is done by the command

$ make doc

6. Installation

If for some reason you don't want to use bedwyr fresh out of the tarball, and you won't or can't use one of the provided packages, you can use the make install facility. It makes good use of the standard $DESTDIR variable, which is an absolute prefix added to all installation paths. You can install all the files in a temporary copy of the file hierarchy by typing

$ make DESTDIR=~/tmpdir install

or in a alternative standard place with

$ ./configure --prefix=/usr/local
$ make
$ make install

7. Distribution