Il s'agit de la transcription de l'algorithme ci-dessus en Prolog. Tous les points de choix (règle à utiliser, ...) présentés dans l'algorithme sont testés séquentiellement par l'interprète Prolog. L'axiôme à reconnaître est transmis à tous les prédicats afin de stopper l'analyse dès que celui-ci est reconnu.