Isabelle Primer for Mathematicians

Bogdan Grechuk

Isabelle Primer for Mathematicians

Bogdan Grechuk

School of Informatics

Research output: Book/Report › Other report

Abstract

This is a quick introduction to the Isabelle/HOL proof assistant, aimed at mathematicians who would like to use it for the formalization of mathematical results.

Original language	English
Publisher	School of Informatics
Publication status	Published - 2010

Access to Document

Isabelle PrimerSubmitted manuscript, 143 KB

http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf

1 Finished

The potential of automated reasoning tools to assist the working mathematician
Bundy, A., Aspinall, D. & Dixon, L.
EPSRC
1/10/10 → 31/12/10
Project: Research

Cite this

@book{ec9e425b118b42a8b082c4d6d43192b1,

title = "Isabelle Primer for Mathematicians",

abstract = "This is a quick introduction to the Isabelle/HOL proof assistant, aimed at mathematicians who would like to use it for the formalization of mathematical results.",

author = "Bogdan Grechuk",

year = "2010",

language = "English",

publisher = "School of Informatics ",

}

TY - BOOK

T1 - Isabelle Primer for Mathematicians

AU - Grechuk, Bogdan

PY - 2010

Y1 - 2010

N2 - This is a quick introduction to the Isabelle/HOL proof assistant, aimed at mathematicians who would like to use it for the formalization of mathematical results.

AB - This is a quick introduction to the Isabelle/HOL proof assistant, aimed at mathematicians who would like to use it for the formalization of mathematical results.

M3 - Other report

BT - Isabelle Primer for Mathematicians

PB - School of Informatics

ER -

Isabelle Primer for Mathematicians

Abstract

Access to Document

Projects

The potential of automated reasoning tools to assist the working mathematician

Cite this