Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic. This work presents two provers for basic hybrid logic HL(@), which have been implemented with the aim of comparing the internalised tableau calculi independently proposed, respectively, by Bolander and Blackburn  and Cerrito and Cialdea Mayer . Experimental results are reported, evaluating, from the practical point of view, the different treatment of nominal equalities of the two calculi.
Keywords for this software
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
- Cialdea Mayer, Marta; Cerrito, Serenella: Herod and Pilate: two tableau provers for basic hybrid logic (2010)
- Bolander, Thomas; Blackburn, Patrick: Termination for hybrid tableaus (2007)