Custom automations in Mizar

DOI10.1007/s10817-012-9266-1zbMath1260.68367OpenAlexW2007976915MaRDI QIDQ1945910

Giuseppe Rosolini, Marco Bright Caminati

Publication date: 17 April 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-012-9266-1

zbMATH Keywords

proof assistantformalization of mathematics\texttt{Mizar} proof verifierautomations

Mathematics Subject Classification ID

Related Items (4)

Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver ⋮ Fermat's little theorem via divisibility of Newton's binomial ⋮ SAT-Enhanced Mizar Proof Checking ⋮ Multiplication-related classes of complex numbers

Uses Software

• MizarMode
• MoMM
• Mizar
• MML

Cites Work

• Unnamed Item
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• On equivalents of well-foundedness. An experiment in MIZAR
• Integrating searching and authoring in Mizar
• Preliminaries to Classical First Order Model Theory
• Mizar’s Soft Type System
• Mathematical Knowledge Management
• Mathematical Knowledge Management

This page was built for publication: Custom automations in Mizar