Home > Research > Publications & Outputs > Basic first-order model theory in Mizar

Research

Associated organisational unit

Text available via DOI:

View graph of relations

Basic first-order model theory in Mizar

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

Published

Standard

Basic first-order model theory in Mizar. / Caminati, Marco Bright.
In: Journal of Formalized Reasoning, Vol. 3, No. 1, 17.12.2010.

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

Harvard

Caminati, MB 2010, 'Basic first-order model theory in Mizar', Journal of Formalized Reasoning, vol. 3, no. 1. https://doi.org/10.6092/issn.1972-5787/1974

APA

Caminati, M. B. (2010). Basic first-order model theory in Mizar. Journal of Formalized Reasoning, 3(1). https://doi.org/10.6092/issn.1972-5787/1974

Vancouver

Caminati MB. Basic first-order model theory in Mizar. Journal of Formalized Reasoning. 2010 Dec 17;3(1). doi: 10.6092/issn.1972-5787/1974

Author

Caminati, Marco Bright. / Basic first-order model theory in Mizar. In: Journal of Formalized Reasoning. 2010 ; Vol. 3, No. 1.

Bibtex

@article{84f9108b2e7740cfab4ed06c6ed993fd,
title = "Basic first-order model theory in Mizar",
abstract = "The author has submitted to Mizar Mathematical Library a series of five articles introducing a framework for the formalization of classical first-order model theory.In them, Goedel's completeness and Lowenheim-Skolem theorems have also been formalized for the countable case, to offer a first application of it and to showcase its utility.This is an overview and commentary on some key aspects of this setup.It features exposition and discussion of a new encoding of basic definitions and theoretical gears needed for the task, remarks about the design strategies and approaches adopted in their implementation, and more general reflections about proof checking induced by the work done.",
author = "Caminati, {Marco Bright}",
year = "2010",
month = dec,
day = "17",
doi = "10.6092/issn.1972-5787/1974",
language = "English",
volume = "3",
journal = "Journal of Formalized Reasoning",
number = "1",

}

RIS

TY - JOUR

T1 - Basic first-order model theory in Mizar

AU - Caminati, Marco Bright

PY - 2010/12/17

Y1 - 2010/12/17

N2 - The author has submitted to Mizar Mathematical Library a series of five articles introducing a framework for the formalization of classical first-order model theory.In them, Goedel's completeness and Lowenheim-Skolem theorems have also been formalized for the countable case, to offer a first application of it and to showcase its utility.This is an overview and commentary on some key aspects of this setup.It features exposition and discussion of a new encoding of basic definitions and theoretical gears needed for the task, remarks about the design strategies and approaches adopted in their implementation, and more general reflections about proof checking induced by the work done.

AB - The author has submitted to Mizar Mathematical Library a series of five articles introducing a framework for the formalization of classical first-order model theory.In them, Goedel's completeness and Lowenheim-Skolem theorems have also been formalized for the countable case, to offer a first application of it and to showcase its utility.This is an overview and commentary on some key aspects of this setup.It features exposition and discussion of a new encoding of basic definitions and theoretical gears needed for the task, remarks about the design strategies and approaches adopted in their implementation, and more general reflections about proof checking induced by the work done.

U2 - 10.6092/issn.1972-5787/1974

DO - 10.6092/issn.1972-5787/1974

M3 - Journal article

VL - 3

JO - Journal of Formalized Reasoning

JF - Journal of Formalized Reasoning

IS - 1

ER -