Ich arbeite an einem Satzbeweiser höherer Ordnung, dessen Vereinheitlichung das schwierigste Teilproblem zu sein scheint.

Wenn Huets Algorithmus immer noch als Stand der Technik angesehen wird, hat jemand Links zu Erklärungen, die geschrieben wurden, um von einem Programmierer und nicht von einem Mathematiker verstanden zu werden?

Oder sogar Beispiele, wo es funktioniert und der übliche Algorithmus erster Ordnung nicht?