Questions tagged [mizar]

The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. (from Wikipedia)

Filter by
Sorted by
Tagged with
10 votes
1 answer

Is there a Mizar-like sublanguage for Coq?

Isabelle has the frontend Isar which mimics some features of the Mizar system. I'm curious if Coq has anything similar, i.e. an alternative to tactic scripts that's designed to be readable or similar ...
Greg Nisbet's user avatar
  • 2,671