• niveau de détail dans les preuves formelles
  en mathématiques, on fait la différence entre les arguments "essentiels" et ceux qui sont "évidents" au niveau où on se place
  

• gestion des conditions de bord
  exemple : représentation des droites
  la droite (AB) existe ssi A<>B
  la droite (CD) est confondue avec (AB) si C<>D et C et D sont alignés avec A et B

• gestion des cas dégénérés
  points confondus ou points alignés
  cas générique partie mineure de la preuve formelle

=> automatisation (langage LTac)

JFLA 2004 — F. GUILHOT