Two tableau provers for basic hybrid logic
Marta Cialdea Mayer, Serenella Cerrito, Emanuele Benassi, Fabio Giammarinaro, Chiara Varani · 2009
loop-checking and with any rule application strategy. The two systems were independently proposed, respectively, by Bolander and Blackburn [1] and Cerrito and Cialdea Mayer [2]. The comparison is carried out both from the theoretical point of view and on the practical side. The two calculi bear strong similarities that are highlighted in the paper. They do differ, however, in the treatment of nominal equalities, which in [1] is elegant and simple, while in [2] is more technically involved, using, in fact, explicit substitution and nominal deletion. As a matter of fact, nominal deletion is the crucial difference with the treatment of equalities in the tableau system for hybrid logic previously proposed by van Eijck [10]. In order to evaluate the impact of the different approaches to nominal equalities of the considered calculi, they have been implemented and their performances compared. This work describes the implementations and the results of the empirical evaluation, which shows that substitution and nominal deletion, although unelegant from the theoretical point of view, has meaningful practical advantages. 2 1