This page contains some of the research software developed in AIICS that is currently available for academic use only.
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.
[No longer supported]Download VITAL »
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.
[No longer supported]Use DLS online »
Page responsible: Patrick Doherty
Last updated: 2020-06-11