Shanduro 8.12 yakaburitswa (yazvino iripo diki vhezheni panguva yekunyora nhau ndeye 8.12.1) ye interactive theorem kuratidza chishandiso Coq (cockerel).
Coq inosanganisira iyo Gallina (huku) inotsamira mhando yekuronga mutauro, iyo yakavakirwa padzidziso yekuvaka calculus.
Iyo Coq sisitimu inobvumidza iwe kugadzira ese ari maviri-anotariswa theorem humbowo uye zvirongwa pamwe nehumbowo hwekuenderana kune yakatarwa.
Iyo vhezheni itsva yakavandudza zvakanyanya raibhurari yakajairwa uye zvinyorwa, uye zvakare yakagadzirisa akati wandei zvikanganiso.
Source: linux.org.ru