A forward internal calculus for model generation in S4