machine-checked proof

(также machine-checked theorem proving)
  1. доказательство [теоремы, теорем] под контролем (при помощи) компьютера

#

доказательство теоремы с помощью программы под названием proof assistant (помощник в проведении доказательства), которая гарантирует, что данное доказательство будет подчиняться (не будет противоречить) аксиомам математики и правилам логики. Синоним – computer-assisted proof.

Связные термины

axiom, theorem proving

Все термины