contains the Objective Caml source code
for a counter-model generator
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
The file COPYING details the origin of the
different parts of the source code.
Do not hesitate to contact me at email@example.com
for further information.
modified on June the 18th 2004.