scientific article; zbMATH DE number 1863397
From MaRDI portal
Publication:4790672
zbMath1005.68539MaRDI QIDQ4790672
Publication date: 4 February 2003
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2152/21520378
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (17)
Four decades of {\textsc{Mizar}}. Foreword ⋮ Improving legibility of formal proofs based on the close reference principle is NP-hard ⋮ Mizar: State-of-the-art and Beyond ⋮ A Brief Overview of Mizar ⋮ A proof-centric approach to mathematical assistants ⋮ A Declarative Language for the Coq Proof Assistant ⋮ Audience role in mathematical proof development ⋮ A certified proof of the Cartan fixed point theorems ⋮ Declarative Proof Translation (Short Paper) ⋮ On the Structure of Mizar Types ⋮ A revision of the proof of the Kepler conjecture ⋮ From LCF to Isabelle/HOL ⋮ Composable Discovery Engines for Interactive Theorem Proving ⋮ The Isabelle/Naproche natural language proof assistant ⋮ An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Formalizing Arrow's theorem
Uses Software
This page was built for publication:
