An example of formalizing recent mathematical results in MIZAR
From MaRDI portal
Publication:865630
DOI10.1016/j.jal.2005.10.003zbMath1107.68100OpenAlexW2045864901MaRDI QIDQ865630
Publication date: 20 February 2007
Published in: Journal of Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jal.2005.10.003
Related Items
Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver ⋮ Mizar: State-of-the-art and Beyond ⋮ Isabelle formalisation of original representation theorems ⋮ Prime factorization of sums and differences of two like powers ⋮ SAT-Enhanced Mizar Proof Checking
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A compendium of continuous lattices in MIZAR
- The geometry of generalized Veronese spaces
- On Better-Quasi-Ordering Countable Series-Parallel Orders
- Mathematical Knowledge Management
- On Segre's product of partial line spaces and spaces of pencils