"Il existe des classes computationnelles où les algorithmes de preuves sont tractables (voire simplement décidables) mais ce sont des cas restreints et peu pratiques pour l'informatique "réelle"."
En refactorant cette phrase, problème de consistance :)....... je voulais dire :
"Les preuves sur la majorité des classes computationnelles de l'informatique "réelle" sont intractables, voire indécidables."
[^] # Re: prouveur automatique/assistant de preuve
Posté par smc . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 1.
En refactorant cette phrase, problème de consistance :)....... je voulais dire :
"Les preuves sur la majorité des classes computationnelles de l'informatique "réelle" sont intractables, voire indécidables."