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): http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/eshol05.pdf
This is free software, licensed under GPL version 2. A copy of this
license can be found in COPYING or, depending on your distribution,
Released sources and binaries may be obtained from https://gforge.inria.fr/frs/?group_id=367 and packages from http://slimmer.gforge.inria.fr/bedwyr/#download.
Development sources may be obtained via the commands
svn checkout svn://scm.gforge.inria.fr/svn/slimmer
svn checkout --username anonsvn https://scm.gforge.inria.fr/svn/slimmer
(the password is the username).
The project is also available as an opam package, and for Debian
http://slimmer.gforge.inria.fr/releases/debian/ squeeze main), Gentoo
(public user overlay
dawan) and Windows. The Linux packages contains
the core libraries as well as the complete program.
For proper compilation and installation, a Linux environment and the following packages are required:
OCaml-3.12.1(or later) and
findlib(sometimes packaged as ocamlfind)
bzip2and some other standard tools
With the vanilla archive, the single command
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
./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
and type "#help." for a little help.
doc/quickstart.(pdf|html): more information on how to use bedwyr
doc/refman/index.html: complete system description
_build/src.docdir/index.html: source code 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
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
Vim and Emacs files.
A few simple examples.
Code for the unification and non-destructive normalization of LLambda. Also contains a term indexing module, currently only used for tabling.
Generic low-level input/output functions.
Construction of a typed parse tree (lexer and parser), transformation to an untyped but type-checked abstract syntax tree.
Tabling, environments and proof-search procedure.
Optional functionallies (XML proof export).