Home > Research > Publications & Outputs > Custom automations in Mizar

Research

Associated organisational unit

Text available via DOI:

View graph of relations

Custom automations in Mizar

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Published

Standard

Custom automations in Mizar. / Caminati, Marco Bright; Rosolini, Giuseppe.
In: Journal of Automated Reasoning, Vol. 50, 01.11.2012, p. 147–160.

Research output: Contribution to Journal/Magazine › Journal article › peer-review

Harvard

Caminati, MB & Rosolini, G 2012, 'Custom automations in Mizar', Journal of Automated Reasoning, vol. 50, pp. 147–160. https://doi.org/10.1007/s10817-012-9266-1

APA

Caminati, M. B., & Rosolini, G. (2012). Custom automations in Mizar. Journal of Automated Reasoning, 50, 147–160. https://doi.org/10.1007/s10817-012-9266-1

Vancouver

Caminati MB, Rosolini G. Custom automations in Mizar. Journal of Automated Reasoning. 2012 Nov 1;50:147–160. doi: 10.1007/s10817-012-9266-1

Author

Caminati, Marco Bright ; Rosolini, Giuseppe. / Custom automations in Mizar. In: Journal of Automated Reasoning. 2012 ; Vol. 50. pp. 147–160.

Bibtex

@article{7eac9a49480e491da0f4c44e672eea28,
title = "Custom automations in Mizar",
abstract = "The central aim of the Mizar project is to produce strictly formalized mathematical statements with mechanically certified proofs. When writing a Mizar formalization, a significant amount of the user{\textquoteright}s time typically goes into browsing the Mizar Mathematical Library (MML) for the already-proved results he needs. Here a few techniques to reduce this time are illustrated.",
author = "Caminati, {Marco Bright} and Giuseppe Rosolini",
year = "2012",
month = nov,
day = "1",
doi = "10.1007/s10817-012-9266-1",
language = "English",
volume = "50",
pages = "147–160",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",

}

RIS

TY - JOUR

T1 - Custom automations in Mizar

AU - Caminati, Marco Bright

AU - Rosolini, Giuseppe

PY - 2012/11/1

Y1 - 2012/11/1

N2 - The central aim of the Mizar project is to produce strictly formalized mathematical statements with mechanically certified proofs. When writing a Mizar formalization, a significant amount of the user’s time typically goes into browsing the Mizar Mathematical Library (MML) for the already-proved results he needs. Here a few techniques to reduce this time are illustrated.

AB - The central aim of the Mizar project is to produce strictly formalized mathematical statements with mechanically certified proofs. When writing a Mizar formalization, a significant amount of the user’s time typically goes into browsing the Mizar Mathematical Library (MML) for the already-proved results he needs. Here a few techniques to reduce this time are illustrated.

U2 - 10.1007/s10817-012-9266-1

DO - 10.1007/s10817-012-9266-1

M3 - Journal article

VL - 50

SP - 147

EP - 160

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

ER -