sl_disprove
sl_disprove
is a heuristic procedure for disproving SL entailments.
The tool and the theory behind it is described in the [TABLEAUX15] paper.
Compiling
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.
Running
$ sl_disprove.native
will print out instructions for use.
Example
Is a linked-list segment from x
to y
also a linked-list segment from y
to x
?
$ ./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 x
to y
isn’t (in general) a chain from y
to x
.
Benchmarks in TABLEAUX15
There are three classes of benchmarks described in the paper. The classes SLL and UDP are from the SL-COMP14 competition and can be obtained from the SL-COMP14 GitHub repository.
The third class, LEM, is included in the Cyclist repository, under benchmarks/sl_disproof
.
The definitions are in all.defs
and the sequents in seqs
. The invbench.sh
script will execute the LEM benchmark.