Pilate and Herod:
two tableau provers for basic hybrid logic

(superseded by Sibyl)

Università di Roma Tre


Pilate and Herod are the implementations of two internalized tableau calculi for HL(@), both terminating without loop-checking and with no restriction on the rule application ordering. The two calculi were independently proposed, respectively, by Bolander and Blackburn [1] and Cerrito and Cialdea Mayer [2].

The systems essentially differ in the treatment of nominal equalities. Experiments carried out with the two provers have shown that the approach implemented by Herod, altough theoretically less elegant than Pilate's, has important practical advantages.

The two systems and the first experimental results are described in [3]. New experiments are reported in [4]. [6] is a revised and extended version of [2]. The other works cited in the references are extensions of the calculus implemented in Herod.



Download



References

  1. T. Bolander and P. Blackburn. Termination for hybrid tableaus. Journal of Logic and Computation, 2007.

  2. S. Cerrito and M. Cialdea Mayer. Terminating tableaux for HL(@) without loop-checking. Technical Report IBISC-RR-2007-07, Ibisc Lab., UniversitÚ d'Evry Val d'Essonne, 2007.

  3. M. Cialdea Mayer, S. Cerrito, E. Benassi, F. Giammarinaro, C. Varani. Two tableau provers for basic hybrid logic. Technical Report RT-DIA-145-2009, Dipartimento di Informatica e Automazione, UniversitÓ di Roma Tre, 2009.

  4. M. Cialdea Mayer, S. Cerrito. Herod and Pilate: two tableau provers for basic hybrid logic. J. Giesl and R. Haehnle (Eds.): IJCAR 2010, LNAI 6173, pp. 255-262, 2010.
    Abstract    Draft

  5. S. Cerrito, M. Cialdea Mayer. Tableaux with Substitution for Hybrid Logic with the Global and Converse Modalities. Technical Report RT-DIA-155-2009, Dipartimento di Informatica e Automazione, UniversitÓ di Roma Tre, 2009.

  6. S. Cerrito, M. Cialdea Mayer. An efficient approach to nominal equalities in hybrid logic tableaux, Journal of Applied Non-Classical Logics (2010), 20(1-2):39-61 (a revised and extended version of [2]).
    Abstract    Draft

  7. M. Cialdea Mayer, S. Cerrito. Nominal Substitution at work with the Global and Converse Modalities. L. Beklemishev, V. Goranko and V. Shehtman (Eds.): Advances in Modal Logic, volume 8, College Publications, pp. 57-74, 2010.
    Abstract    Draft