The Sibyl Prover

Sibyl is an automated theorem prover for multi-modal hybrid logic with binders, converse, global and graded modalities, transitivity assertions and relation hierarchies.

It is based on a tableau calculus that is provably terminating and complete, provided that the input formulae satisfy some restrictions on the occurrences of the binder, ensuring that they belong to a decidable fragment of the considered logic.

The works lying Sibyl's theoretical basis are cited in the Publications page.

Sibyl is implemented in Objective Caml and runs under Linux. Some parts of its implementation code are inherited from its predecessor, Herod.