Demostració interactiva de teoremes
 |
S'ha sugerit que est artícul o secció siga fusionat en [[::Provador de teoremes llògiques|Provador de teoremes llògiques]] . (Discussió). Una volta hages realisat la fusió d'artículs, demana la fusió d'historials en WP:TAB/F. |
La demostració interactiva de teoremes és un camp de la ciència computacional i la llògica matemàtica relatiu a les ferramentes per a desenrollar proves formals per a la colaboració home-màquina. Açò involucra una espècie de assistent de proves: un editor interactiu de proves, o una atra interfaç, en la qual un home puga guiar la busca de proves, els detalls que estan almagasenades en elles, i alguns dels passos oferits per, un ordenador.
Eixemples:
- Demostradores de teoremes HOL (per eixemple, Isabelle)
- Prototip de sistema de verificació (PVS)
- Coq
- PhoX
- MINLOG
Vore també
[editar | editar còdic]
- Este artícul conté una traducció derivada de «Demostración interactiva de teoremas» de Wikipedia en castellà publicada baix la Llicència de documentació lliure de GNU i la Llicència Creative Commons Reconeiximent-CompartirIgual 4.0 Internacional.