This package
contains the Objective Caml source code
for a counter-model generator
for propositional
Gödel-Dummett logic. It is based on ideas developed
in the following paper accepted to IJCAR 2004:
A more pratical description of the algorithm is presented
in the following paper accepted to the ENTCS electronic
journal Disproving. It comes
as a complement to the previous theoretical paper:
This is a prototype implementation. Just type
"make" to compile the project. A command-line
tool is then available: "cmodels". It reads
formulae from standard input. An optional
loglevel can be set by the [-log] option.
The file "examples.ml" contains a list of
commands to test the generator interactively
under Ocaml. Consult this file for the syntax
of formulae.
The file COPYING details the origin of the
different parts of the source code.
Do not hesitate to contact me at larchey@loria.fr
for further information.
Last
modified on June the 18th 2004.