sl_disprove is a heuristic procedure for disproving SL entailments.
The tool and the theory behind it is described in the [TABLEAUX15] paper.
If you are simply looking for the latest version of
sl_disprove, have a look at Installation.
If you want to try out the original version underpinning the [TABLEAUX15] paper, then you can download an archive including x86_64 binaries and the original benchmark suite at the TABLEAUX15 GitHub release.
will print out instructions for use.
Is a linked-list segment from
y also a linked-list segment from
$ ./sl_disprove.native -S "ls(x,y) |- ls(y,x)" INVALID: ls^1(x, y) |- ls^2(y, x)
No, because the chain of pointers from
y isn’t (in general) a chain from
Benchmarks in TABLEAUX15
The third class, LEM, is included in the Cyclist repository, under
The definitions are in
all.defs and the sequents in
script will execute the LEM benchmark.