Andrzej Trybulec

Andrzej Wojciech Trybulec (29 de enero de 1941 en Cracovia , Polonia – 11 de septiembre de 2013 en Białystok , Polonia ) fue un matemático e informático polaco conocido por su trabajo en el sistema Mizar . ^{[ 1 ]}

Sus padres, Jan W. Trybulec y Barbara H. Kurlus, eran farmacéuticos de profesión y regentaban una farmacia en Szczucin , un pequeño pueblo cerca de Tarnów , en el sureste de Polonia, donde dispensaban medicamentos. Cursó el bachillerato en Ruda Śląska y, posteriormente, por iniciativa propia, se trasladó a un prestigioso instituto de Cracovia , donde obtuvo el título de bachillerato. Estudió matemáticas en la Universidad de Varsovia , donde impartió clases en la cátedra de Geometría de 1964 a 1966 y se doctoró en 1966. Hasta 1967 fue profesor en el Instituto de Matemáticas de la Universidad de Varsovia, y de 1967 a 1971 fue profesor adjunto en la Universidad Tecnológica de Varsovia . Desde 1971 trabajó en el Instituto de Biblioteconomía y Ciencias de la Información de la misma universidad. En septiembre y octubre de 1973, Trybulec fue profesor visitante en el Instituto Panruso de Información Científica y Técnica (VINITI) en Moscú , entonces parte de la URSS , donde concibió la idea de la legibilidad por máquina de un texto matemático. Obtuvo su doctorado en 1974 en el Instituto de Matemáticas de la Academia Polaca de Ciencias, bajo la dirección de Karol Borsuk .

Los primeros trabajos matemáticos de Trybulec versaron sobre diversos temas de topología y espacios métricos , temas que Karol Borsuk había impulsado . Paralelamente a su investigación topológica general , también trabajó en lingüística computacional y semántica de lenguajes de programación . Aplicando el marco de los axiomas de la teoría de conjuntos de Tarski-Grothendieck , esencialmente la teoría de conjuntos de Zermelo-Fraenkel complementada con el axioma de Tarski, donde todos los objetos son conjuntos y se elimina la noción de clase, junto con la lógica de primer orden de la deducción natural de Gentzen - Jaśkowski , en 1973 diseñó el sistema de formalización Mizar, que consta de un lenguaje formal para escribir definiciones y demostraciones matemáticas, y un asistente de demostración capaz de verificar mecánicamente las demostraciones escritas en dicho lenguaje. Aunque la primera presentación del sistema Mizar el 14 de noviembre de 1973 en un seminario del Instituto de Biblioteconomía e Información Científica fue entendida más como una especulación visionaria que como un proyecto de investigación, su idea fue posteriormente desarrollada por él mismo y sus colaboradores hasta convertirse en la Biblioteca Matemática Mizar (MML), una biblioteca de matemáticas formalizadas que puede utilizarse en la demostración de nuevos teoremas y el mayor repositorio mundial de matemáticas formalizadas y verificadas por ordenador. Desde 1978 hasta su fallecimiento, impartió clases como profesor en el Instituto de Informática de la Universidad de Białystok , y entre 1984 y 1985 fue profesor visitante en el Departamento de Informática e Ingeniería de la Universidad de Connecticut . Publicó numerosos artículos, principalmente en la revista Formalized Mathematics, dedicada a las contribuciones a la MML.

• Asperti, Andrea; Bancerek, Grzegorz; Trybulec, Andrzej, eds. (2004), Gestión del conocimiento matemático: Actas de la Tercera Conferencia Internacional, MKM 2004, Białowieża, Polonia, 19-21 de septiembre de 2004 , Lecture Notes in Computer Science 3119 , Nueva York: Springer, ISBN 978-3-540-23029-8

• Sistema Mizar
• Cronología de la ciencia y la tecnología polacas
• Lista de matemáticos polacos
• Lista de personas polacas

• Kuperberg, Krystyna Trybulec (septiembre de 2015), "Andrzej Trybulec – in Memoriam" , Journal of Automated Reasoning , 55 (3): 187–190 , doi : 10.1007/s10817-015-9343-3
• Matuszewski, Roman; Zalewska, Anna, eds. (2007), «From Insight to Proof: Festschrift in Honour of Andrzej Trybulec» (PDF) , Studies in Logic, Grammar and Rhetoric , vol.  10, ISBN 978-837431128-1
• Matuszewski, Roman; Rudnicki, Piotr (marzo de 2005), "Mizar: Los primeros 30 años" (PDF) , Matemáticas Mecanizadas y sus Aplicaciones , 4 ( 1): 3–24
• Rudnicki, Piotr (1992), "Una visión general del proyecto Mizar", en Nordström, Bengt; Petersson, Kent; Plotkin, Gordon (eds.), Actas del Taller de 1992 sobre Tipos para Pruebas y Programas, Bästad, Suecia, junio de 1992 , Båstad : Universidad Tecnológica de Chalmers , pp. 311–330 

• "Andrzej Trybulec", Universidad de Bialystok
• Andrzej Trybulec en el Proyecto de Genealogía Matemática
• Sistema Mizar http://mizar.uwb.edu.pl
• http://math.uwb.edu.pl/~trybulec/awards.html
• https://web.archive.org/web/20060927204402/http://markun.cs.shinshu-u.ac.jp/mizar/mma.dir/2005/mma2005(2).pdf
• http://www-history.mcs.st-and.ac.uk/Biographies/Kuperberg.html
• http://mizar.uwb.edu.pl/cgi-bin/andrzej/memento
• http://www.openmath.org/meetings/eindhoven2003/proceedings/trybulec.pdf