Pilate and Herod:
two tableau provers for basic hybrid logic

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

• Pilate and Herod (Linux binaries)
• The test set of hand-written formulae used in the comparison described in [3].
• A set of formulae randomly generated by HGen, used for new tests. The tar-gzipped file contains four subdirectories, distinguishing the sets of formulae by their modal depth. Each subdirectory contains the .hgenrc file used for the generation and different subdirectories, each of which contains 50 tests with the same number of clauses (60 to 200). The results are reported in [4].

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