Jeśli jesteś właścicielem tej strony, możesz wyłączyć reklamę poniżej zmieniając pakiet na PRO lub VIP w panelu naszego hostingu już od 4zł!
Strony WWWSerwery VPSDomenyHostingDarmowy Hosting CBA.pl
M a r i u s z     G i e r o



EDUCATION
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'.
RESEARCH INTERESTS
computer oriented formalization of mathematics (Mizar, Coq), type theory
RESEARCH VISITS
  1. Shinshu University, Nagano, Japan, 01-02.2013.
  2. University of Nijmegen ( 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.
PUBLICATIONS (bibtex)

[0]   2014-2016

[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/

[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/

[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/

[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.

[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/

[14]   M. Giero, F. Wiedijk, MMode, a Mizar Mode for the proof assistant Coq, Tech. rep., ICIS, Radboud Universiteit Nijmegen (2004).

MEMBERSHIP IN ACADEMIC SOCIETIES
Association of Mizar Users