La herramienta ‘THeM’ fue creada como trabajo de final de dos materias de segundo año de una carrera de Informática. Esta permite, dado un conjunto de cláusulas de la Lógica de Predicados de Primer Orden, determinar la existencia de Modelos de Herbrand para las mismas (lo cual permite conocer su satisfacibilidad). La herramienta provee una interfaz sencilla de utilizar y de entender, ya que uno de los objetivos es que sea usada por futuros alumnos de materias que estudien el tema.