Publications
The first work defining the basic calculus on which Sibyl is based is
[1],
where only basic hybrid logic is considered. In [2]
the calculus is extended to treat the global and converse modalities,
[3]
further extends it to handle transitivity and relation hierarchies,
and [4] treats the case of the graded modalities.
Full proofs of the termination and completeness theorems stated in
[3] can be found in its extended version.
-
S. Cerrito, M. Cialdea Mayer.
A
Tableau Based Decision Procedure for a Broad Class of
Hybrid Formulae with Binders.
K. Brünnler and G. Metcalfe (Eds.):
Automated Reasoning with Analytic Tableaux and Related Methods
(TABLEAUX 2011), LNAI 6793, Springer Verlag, pp. 104-118, 2011.
Abstract
Draft
-
S. Cerrito, M. Cialdea Mayer.
A Tableau Based Decision Procedure
for an Expressive Fragment of
Hybrid Logic with Binders, Converse and Global Modalities.
Journal of Automated Reasoning,
51(2):197-239, 2013.
Abstract
Draft
-
M. Cialdea Mayer.
A Proof Procedure for Hybrid Logic with
Binders, Transitivity and Relation Hierarchies.
24th Conference on Automated Deduction (CADE 2013),
LNCS 7898, Springer, pp. 76-90, 2013.
Abstract
Draft
Errata Corrige
Slides
illustrating the calculus
in action
Extended version.
-
M. Cialdea Mayer.
Extended Decision Procedure for a Fragment of HL with Binders.
Journal of Automated Reasoning, 53 (3): 305-315, 2014.
Abstract.
Draft.
Erratum.