M a r i u s z     G i e r o


University of Bialystok
Chair of Logic, Informatics and Philosophy of Science
Plac Uniwersytecki 1, p. 44
15-420 Bialystok, Poland
phone   +48 85 745 75 07
e-mail:    giero@uwb.edu.pl
www:    http://logika.uwb.edu.pl/mg/homepage

Ph.D. in computer science in 2013, Shinshu University, Nagano, Japan.
Thesis: 'An extension of the Basic Propositional Linear Temporal Logic by the very strict until operator: a Formalization in Mizar'.

M. Sc. in mathematics in 1996, Warsaw University, Bialystok Branch.
Thesis: 'The properties of product of family of many sorted algebras'.
computer oriented formalization of mathematics (Mizar, Coq), type theory
  1. Shinshu University, Nagano, Japan, 01-02.2013.
    E-learning course on Temporal Logic with the use of the Mizar system.
  2. University of Nijmegen (Foundations Research Group - Subfaculty of Computing Science), The Netherlands.
    1.01.2003 - 31.12.2003 as a Young Visiting Researcher of the Calculemus Project.
    "Mizar mode" for Coq (providing Coq with a mathematical proof style language based on the Mizar system), Description of the system, Download the system.

[1]   M. Giero, The Derivations of Temporal Logic Formulas, Formalized Mathematics 20 (3) (2012) 215–219.

[2]   M. Giero, The Properties of Sets of Temporal Logic Subformulas, Formalized Mathematics 20 (3) (2012) 221–226.

[3]   M. Giero, Weak Completeness Theorem for Propositional Linear Time Temporal Logic, Formalized Mathematics 20 (3) (2012) 227–234.
URL http://www.degruyter.com/view/j/forma.2012.20.issue-3/v10037-012-0027-8/v10037-012-0027-8.xml?format=INT

[4]   M. Giero, The Axiomatization of Propositional Linear Time Temporal Logic, Formalized Mathematics 19 (2) (2011) 113–119.
URL http://www.degruyter.com/view/j/forma.2011.19.issue-2/v10037-011-0018-1/v10037-011-0018-1.xml?format=INT

[5]   M. Giero, Formalization of propositional linear temporal logic in the Mizar System, Studies in Logic, Grammar and Rhetoric 22 (35) (2010) 7–21.
URL http://logika.uwb.edu.pl/studies/vol35.html

[6]   M. Giero, Application of Bitemporal Databases on Medical Data, Studies in Logic, Grammar and Rhetoric 17 (30) (2009) 193–211.
URL http://logika.uwb.edu.pl/studies/vol30.html

[7]   M. Giero, Querying Temporal Database with the Language of First-Order Temporal Logic, Studies in Logic, Grammar and Rhetoric 11 (24) (2007) 85–93.
URL http://logika.uwb.edu.pl/studies/vol24.html

[8]   M. Giero, On the General Position of Special Polygons, Formalized Mathematics 10 (2) (2002) 89–95.

[9]   M. Giero, Hierarchies and Classifications of Sets, Formalized Mathematics 9 (4) (2001) 865–869.
URL http://fm.mizar.org/2001-9/fm9-4.html

[10]   M. Giero, More on Products of Many Sorted Algebras, Formalized Mathematics 5 (4) (1996) 621–626.
URL http://fm.mizar.org/1996-5/fm5-4.html

[11]   M. Giero, R. Matuszewski, Some Special Sequences of Points on the Plane, Mechanized Mathematics and Its Application 1 (6) (2007) 55–62.
URL http://logika.uwb.edu.pl/mg/homepage/mechanized.pdf

[12]   M. Giero, R. Matuszewski, Lower Tolerance. Preliminaries to Wroclaw Taxonomy, Formalized Mathematics 9 (3) (2001) 597–603.
URL http://fm.mizar.org/2001-9/fm9-3.html

[13]   M. Giero, R. Milewski, Storing and Retrieving Information on the Treatment of Infertility with the Use of the Bitemporal Database and Temporal Logic, Studies in Logic, Grammar and Rhetoric 17 (30) (2009) 213–223.
URL http://logika.uwb.edu.pl/studies/vol30.html

[14]   M. Giero, F. Wiedijk, MMode, a Mizar Mode for the proof assistant Coq, Tech. rep., ICIS, Radboud Universiteit Nijmegen (2004).
URL http://logika.uwb.edu.pl/mg/homepage/mmode.pdf

Mizar course in temporal logic on Moodle
Association of Mizar Users
Polish Association for Logic and Philosophy of Science

html-linked Mizar articles
Automated Reasoning for Mizar
Mizar Bibliography
Skeleton of Mizar Proofs
MML Query
Mizar: useful resorces - Japan site
Foundation of Mathematics for Computer-Aided Formalization
ICM, Web of Science
Web of Knowledge