Sibyl is an automated theorem prover for multi-modal hibrid logic with binders, the converse and global modalities, transitivity assertions and relation hierarchies. It is based on a tableau calculus that is provably terminating and complete, provided that the negation normal form of the formulae given in input do not contain any occurrence of the binder that is both in the scope and contains in its scope a universal operator. 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.
Keywords for this software
References in zbMATH (referenced in 6 articles , 2 standard articles )
Showing results 1 to 6 of 6.
- Cialdea Mayer, Marta: A prover dealing with nominals, binders, transitivity and relation hierarchies (2020)
- Mayer, Marta Cialdea: Extended decision procedure for a fragment of HL with binders (2014)
- Cerrito, Serenella; Mayer, Marta Cialdea: A tableau based decision procedure for an expressive fragment of hybrid logic with binders, converse and global modalities (2013)
- Cialdea Mayer, Marta: A proof procedure for hybrid logic with binders, transitivity and relation hierarchies (2013)
- Cerrito, Serenella; Cialdea Mayer, Marta: A tableaux based decision procedure for a broad class of hybrid formulae with binders (2011)
- Cerrito, Serenella; Mayer, Marta Cialdea: An efficient approach to nominal equalities in hybrid logic tableaux (2010)
Further publications can be found at: http://cialdea.dia.uniroma3.it/sibyl/publications.php