- ajouter un warning pour les règles non reconnues
- problème du cas ite pour eq_congruent ?
- traduire input
- relire :
scope.ml proof.ml translate.ml view.ml verine.ml
- il existe un ordre strict sur les termes dans veriT utilisé pour orienter les égalités
- on suppose que la conclusion de l’input contient toutes les variables libres de la preuve
- on suppose que l’ordre des propositions est conservé dans résolution
- on suppose dans une résolution c1 c2 … cn que pour tout i, il n’existe qu’une seule proposition p telle que p est dans ci et non p est dans c(i+1) ou inversement
- définitions non acceptées (fonction equal non adaptée pour cela)