A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies
Jimmy Thomson (ANU)
LOGIC AND COMPUTATION SEMINARDATE: 2013-06-04
TIME: 14:00:00 - 14:30:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
A tableau calculus constituting a decision procedure for hybrid logic with the converse modalities, the global ones and a restricted use of the binder has been defined in a previous paper. This work shows how to extend such a calculus to multi-modal logic equipped with two features largely used in description logics, i.e. transitivity and relation inclusion assertions. An implementation of the proof procedure is also briefly presented, along with the results of some preliminary experiments.
