Deftab, a tableau-based intuitionistic prover with defaults

How to compile

You need:

  • ghc 8.4 or newer
  • cabal-install 2.4 or newer

Compilation steps:

  • go to the directory that contains the file deftab.cabal
  • run cabal install and wait

How to run

Where is the binary:

  • the deftab executable will be copied to the default Cabal binary folder, which is ~/.cabal/bin under Linux.
  • it is also available from the current directory (where deftab.cabal can be found) at path ./dist/build/deftab/deftab.

To get help about deftab's options run: deftab --help.

The simplest way to see deftab run with an example formula is, for instance:

  • deftab -f ./examples/theorem.01.dt