Rövid szöveges bemutatás:
Az ITOU egy bizonyító rendszer volt, melyet Rouveirol és Puget alkottak meg 1989-ben. Az ITOU a konkrét dolgoktól haladt az általánosítás felé. Elfogadta a definit klózokat, mint pozitív bizonyíték. Nem képes azonban saját magától új változókat bevezetni, csak a pozitív bizonyítékokban lévőeket felhasználni.