A Tableau Proof System for the Spatial Qualification Logic

Abstract

Spatial Qualification Model (SQM) is a logical system built to reason about the possibility of an agent’s presence at a location of incidence, at a certain time given its prior antecedents. The usability of this logical system is strongly dependent on the existence of a proof system. This work is aimed at developing an analytic proof system to demonstrate the logical truth of statements in the spatial qualification logic. Tableau proof method was used to analytically prove that the formulae (axioms) in the SQM system were the logical consequence of the set of formulae that make up the prior knowledge. The proof system confirms the logical truth of the axioms in the system.