Abstract

Qualitative description of movements can be very important for representation and reasoning about dynamic systems which are complex in structure or whenever numerical data are incomplete or inaccessible. For this reason, we present a hybrid approach based on the combination of qualitative reasoning, quantitative data and logical methods. In this article, we introduce a new propositional dynamic logic QM for representation and reasoning with relative movements of objects. In this way, we can infer additional information about movements by using axioms and the logic apparatus. We present a sound and complete deduction system in dual tableaux style for the logic QM. The system can be used for verification of validity of formulas of the logic in question.