A Relatively Complete Axiomatisation of Projection onto State in the Duration Calculus
Dimitar P. Guelev, Dang Van Hung · Journal of Applied Non-Classical Logics · 2004
We present a complete axiomatisation of the operator of projection onto state in the Duration Calculus (DC) relative to validity in DC without extending constructs. Projection onto state was introduced and studied extensively in our earlier works. We first establish the completeness of a system of axioms and proof rules for the operator relative to validity in the extension of DC by neighbourhood formulas, which express the neighbourhood values of boolean DC state expressions. By establishing a relatively complete axiomatisation for the neighbourhood formulas in DC, we then achieve completeness of our system relative to basic DC.