Deftab: a tableau-based modal prover with defaults

Deftab implements a tableau calculus to handle modal logics with defaults, namely:

• hybrid default logic
• intuitionistic default logic

It handles sceptical consequence check.

Deftab supports normal default rules only (rules where the justification is equal to the consequent).

How to compile

You need:

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

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

Input format examples

Hybrid logic input:

classical

facts:
A(!N5 -> <>N5);
A<>true;

defaults:
T --> N1: <>N2;
T --> N2: !N5;
T --> N2: ([]N2);

consequence:
N1:<><>N5;

Intuitionistic input:

intuitionistic
facts:
P1 v !P1; P1 -> !P2;
(P4 ^ P5 ^ P6) -> P7;
P7 -> P1; P3;
defaults:
P3 --> P2;
consequence:
P2

Intuitionistic input without facts nor defaults (to check validity of given formula):

intuitionistic
consequence:
(P1 & P2) <-> (((P1 v P2) <-> P2) <-> P1)

Commandline flags

  -f --filename=FILE    input file
  -t --timeout=INT      timeout (in seconds, default=none)
     --stats=INT        display statistics every n steps (default=none)
     --strategy=ITEM    specify rules strategy
     --backjumping      enable backjumping (enabled by default)
  -c --cache            enable subtableaux caching (enabled by default)
     --no-defaults      ignore defaults of input file
     --no-facts         ignore facts of input file
  -r --reflexive        for classical input, set models as reflexive
     --transitive       for classical input, set models as transitive
     --bench            run different strategies on input and report times
  -? --help             Display help message
  -V --version          Print version information
     --numeric-version  Print just the version number
  -v --verbose          Loud verbosity
  -q --quiet            Quiet verbosity

Deftab benchmark suite

• See the README.md file in the benchmarks/ directory.