On the Structure of Mizar Types

DOI10.1016/S1571-0661(04)80758-8zbMath1264.03040MaRDI QIDQ4924547

Grzegorz Bancerek

Publication date: 6 June 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (6)

Presentation and manipulation of Mizar properties in an Isabelle object logic ⋮ The Mizar Mathematical Library in OMDoc: translation and applications ⋮ User interaction with the Matita proof assistant ⋮ Flexary connectives in Mizar ⋮ Formalising foundations of mathematics ⋮ Pythagorean tuning: pentatonic and heptatonic scale

Uses Software

• Mizar

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Commutative algebra in the Mizar system
• A compendium of continuous lattices in MIZAR
• A refinement of de Bruijn's formal language of mathematics
• On equivalents of well-foundedness. An experiment in MIZAR

This page was built for publication: On the Structure of Mizar Types