machine-checked proof
(также machine-checked theorem proving)
- доказательство [теоремы, теорем] под контролем (при помощи) компьютера
#
доказательство теоремы с помощью программы под названием proof assistant (помощник в проведении доказательства), которая гарантирует, что данное доказательство будет подчиняться (не будет противоречить) аксиомам математики и правилам логики. Синоним – computer-assisted proof.
Связные термины
axiom, theorem proving