Logic of temporal attribute implications

TL;DR

This paper develops a formal logic for reasoning about temporal attribute dependencies, providing semantic foundations, axiomatizations, and complexity analysis, including decidability results for specific formula classes.

Contribution

It introduces a novel logic for temporal attribute implications, with fixed-point semantics, axiomatizations, and complexity results, including decidability for predictive formulas.

Findings

Entailment is NP-hard and in EXPSPACE.

Axiomatizations and completeness proofs are provided.

Decidability is achieved for predictive formulas in pseudo-linear time.

Abstract

We study logic for reasoning with if-then formulas describing dependencies between attributes of objects which are observed in consecutive points in time. We introduce semantic entailment of the formulas, show its fixed-point characterization, investigate closure properties of model classes, present an axiomatization and prove its completeness, and investigate alternative axiomatizations and normalized proofs. We investigate decidability and complexity issues of the logic and prove that the entailment problem is NP-hard and belongs to EXPSPACE. We show that by restricting to predictive formulas, the entailment problem is decidable in pseudo-linear time.