scientific article; zbMATH DE number 1951640
From MaRDI portal
Publication:4413895
zbMath1022.68622MaRDI QIDQ4413895
Publication date: 21 July 2003
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2594/25940203.htm
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
A new export of the Mizar mathematical library ⋮ MizAR 40 for Mizar 40 ⋮ Translating a Dependently-Typed Logic to First-Order Logic ⋮ MPTP 0.2: Design, implementation, and initial experiments ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ MPTP 0.1 - System Description ⋮ On the Structure of Mizar Types ⋮ MPTP-motivation, implementation, first experiments ⋮ Licensing the Mizar Mathematical Library ⋮ Extracting Higher-Order Goals from the Mizar Mathematical Library ⋮ Experiences from exporting major proof assistant libraries ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
