VITAL is a tool for reasoning about temporal narratives in TAL which combines the power of both symbolic and visual modalities. Narratives may be represented in sequential text form and their models depicted in diagrammatic form in terms of time lines.

The DLS algorithm is a quantifier elimination algorithm which takes an arbitrary second-order logic formula and tries to reduce it to an equivalent first-order formula. The algorithm is based on a generalization of Ackermann's Lemma, and has applications in a number of areas, in particular, the reduction of circumscription axioms.