M a r i u s z G i e r o|
Ph.D. in computer science in 2013, Shinshu University, Nagano, Japan.RESEARCH INTERESTS
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 theoryRESEARCH VISITS
 M. Giero, Weak Completeness Theorem for Propositional Linear Time Temporal Logic, Formalized Mathematics 20 (3) (2012) 227–234.
 M. Giero, The Axiomatization of Propositional Linear Time Temporal Logic, Formalized Mathematics 19 (2) (2011) 113–119.
 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.
Mizar course in temporal logic on MoodleMEMBERSHIP IN ACADEMIC SOCIETIES
Association of Mizar Users
Polish Association for Logic and Philosophy of Science