A small universal model for system executions

The author shows that every consistent set of atomic relations has a unified model of size roughly O(n²). This model can be used to give a simplified proof of completeness of some axioms. He gives several complexity results for deciding the theory of several classes of axiom sets, for both partial models and global-time models, showing many such variations to have the same complexity as transitive closure or matrix multiplication. The author shows that deciding disjunctive axioms is NP-complete for both the global-time and the standard model