Ruy de Queiroz

Ruy de Queiroz

Ruy J. Guerra B. de Queiroz (ur. 11 stycznia 1958 r. w Recife ) jest profesorem nadzwyczajnym na Universidade Federal de Pernambuco i posiada znaczące prace badawcze w dziedzinie logiki matematycznej, teorii dowodu, podstaw matematyki i filozofii matematyki. Jest założycielem Warsztatów Logiki, Języka, Informacji i Obliczeń (WoLLIC), które są organizowane corocznie od 1994 roku, zazwyczaj w czerwcu lub lipcu.

Ruy de Queiroz uzyskał tytuł inżyniera elektryka na Escola Politecnica de Pernambuco w 1980 r., tytuł magistra informatyki na Universidade Federal de Pernambuco w 1984 r. , a doktorat z informatyki na Imperial College w Londynie w 1990 r. który obronił Teorię dowodu rozprawy i programowanie komputerowe. Esej o logicznych podstawach obliczeń .

Profil naukowy

Pod koniec lat 80. Ruy de Queiroz zaproponował przeformułowanie teorii typu Martina-Löfa w oparciu o nowe odczytanie Wittgensteina „znaczenie-to-użycie”, w którym wyjaśnienie konsekwencji danego twierdzenia nadaje znaczenie stała logiczna dominująca w zdaniu. Sprowadza się to do niedialogicznej interpretacji stałych logicznych poprzez wpływ reguł eliminacji na reguły wprowadzania, co znajduje paralelę w dialogu / semantyce gry Paula Lorenzena i Jaakko Hintikki . Doprowadziło to do powstania teorii typu zwanej „znaczeniem jako teorią typu użycia”. Odnosząc się do posługiwania się dictum Wittgensteina, wykazał, że aspekt dotyczący wyjaśniania konsekwencji twierdzenia jest obecny od bardzo dawna, kiedy to w liście do Bertranda Russella , gdzie Wittgenstein odnosi się do uniwersalnego kwantyfikatora, który ma znaczenie tylko wtedy, gdy widzi się, co z niego wynika.

Od późniejszych lat 90. Ruy de Queiroz był zaangażowany, wspólnie z Dovem Gabbayem , w program dostarczania ogólnego opisu funkcjonalnej interpretacji logiki klasycznej i nieklasycznej za pomocą pojęcia dedukcji naturalnej. W rezultacie zaproponowano nowe ujęcia funkcjonalnej interpretacji kwantyfikatora egzystencjalnego, a także pojęcia równości zdań, które umożliwiło przekształcenie koncepcji obliczeń bezpośrednich Richarda Statmana oraz nowatorskie podejście do dychotomia „intensjonalne kontra ekstensjonalne” ujęcia zdaniowej równości poprzez Korespondencja Curry – Howard .

Od początku XXI wieku Ruy de Queiroz badał, wspólnie z Anjoliną de Oliveira, geometryczną perspektywę dedukcji naturalnej opartą na opartym na wykresach opisie symetrycznej dedukcji naturalnej Kneale'a .

Służba profesji

  • członek grupy doradczej ds. Nagrody im. Rolfa Schocka w dziedzinie logiki i filozofii (2008 i 2011) Komitetu Nagrody (Królewska Szwedzka Akademia Nauk);
  • Redaktor naczelny, Logic Journal of the Interest Group in Pure and Applied Logics , Oxford University Press, 1993 – obecnie;
  • Współredaktor, Journal of Computer System and Sciences , koordynator i współzałożyciel (wraz z D. Gabbayem), Interest Group in Pure and Applied Logics (IGPL), izby rozliczeniowej Europejskiego Stowarzyszenia Logiki, Języka i Informacji (FoLLI), 1990 – obecnie;
  • Gościnny redaktor kilku tomów (we współpracy z kilkoma światowej sławy logikami i informatykami, takimi jak John Baldwin, Sergei N. Artemov , Bruno Poizat, Dexter Kozen, Angus Macintyre, Grigori Mints, Wilfrid Hodges, Anuj Dawar, Hiroakira Ono, Makoto Kanzawa, Daniel Leivant, Lev Beklemishev) Annals of Pure and Applied Logic, Theoretical Computer Science, Information and Computation, Journal of Computer System and Sciences, Fundamenta Informaticae, kilka tomów Electronic Notes in Theoretical Computer Science;
  • Twórca i główny organizator cyklu warsztatów WoLLIC ( http://www.cin.ufpe.br/~wollic );
  • członek rady redakcyjnej International Directory of Logicians , D. Gabbay & J. Woods (red.), College Publications;
  • Wybrany członek Rady, Association for Symbolic Logic, 2006-2008.

Kluczowe publikacje

  1. (z de Oliveira, A.) Funkcjonalna interpretacja obliczeń bezpośrednich. Notatki elektroniczne w informatyce teoretycznej 269: 19-40, 2011.
  2. O regułach redukcji, znaczeniu jako zastosowaniu i semantyce teorii dowodu, Studia Logica 90(2):211-247, listopad 2008.
  3.   (z de Oliveira, A.) Geometria dedukcji za pomocą wykresów dowodu. W Logic for Concurrency and Synchronisation, R. de Queiroz (red.), tom 18 serii Trends in Logic, Kluwer Acad. Pub., Dordrecht, lipiec 2003, ISBN 1-4020-1270-5 , s. 3–88.
  4. Znaczenie, funkcja, cel, użyteczność, konsekwencje - pojęcia wzajemnie powiązane. Logic Journal of the Interest Group in Pure and Applied Logics, 9(5):693-734, wrzesień 2001, Oxford Univ. Naciskać.
  5. (z Gabbay, D.) Oznakowane odliczenie naturalne. W logice, języku i rozumowaniu. Essays in Honor of Dov Gabbay, HJ Ohlbach i U. Reyle (red.), tom 5 serii Trends in Logic, Kluwer Academic Publishers, Dordrecht, czerwiec 1999, s. 173–250.
  6. (z de Oliveira, A.) Procedura normalizacji fragmentu równania oznaczonego odliczenia naturalnego. Logic Journal of the Interest Group in Pure and Applied Logics, 7(2):173-215, 1999, Oxford Univ. Naciskać. Pełna wersja referatu wygłoszonego na 2nd WoLLIC'95, Recife, Brazylia, lipiec 1995. Streszczenie ukazało się w Journal of the Interest Group in Pure and Applied Logics 4(2):330-332, 1996.
  7. (z Gabbay, D.) The Functional Interpretation of the Existential Quantifier, w Bulletin of the Interest Group in Pure and Applied Logics 3(2-3):243-290, 1995. (Wydanie specjalne dotyczące dedukcji i języka, redaktor gościnny: Ruth Kempson). Pełna wersja referatu wygłoszonego na Logic Colloquium '91, Uppsala. Streszczenie w JSL 58(2):753-754, 1993.
  8. Normalizacja i gry językowe. W Dialectica 48(2):83-123, 1994. (Wczesna wersja przedstawiona na Logic Colloquium '88, Padwa. Streszczenie w JSL 55:425, 1990.)
  9. (z Gabbay, D.) Rozszerzenie interpretacji Curry'ego-Howarda na logikę liniową, istotną i inną logikę zasobów, w Journal of Symbolic Logic 57 (4): 1319-1365. Referat przedstawiony na Logic Colloquium '90, Helsinki. Streszczenie w JSL 56(3):1139-1140, 1991.
  10. (z Maibaumem, T.) Abstrakcyjne typy danych i teoria typów: teorie jako typy, w Zeitschrift für mathematische Logik und Grundlagen der Mathematik 37: 149-166.
  11. (z Maibaum, T.) Teoria dowodu i programowanie komputerowe, w Zeitschrift für mathematische Logik und Grundlagen der Mathematik 36: 389-414.
  12. Dowód-teoretyczny opis programowania i rola reguł redukcji, w Dialectica 42 (4): 265-282.
  13.   de Queiroz, R. de Oliveira, A. i Gabbay, D.: 2011, Funkcjonalna interpretacja dedukcji logicznej. Tom. 5 serii Postępy w logice. Imperial College Press / World Scientific. ISBN 978-981-4360-95-1 .

Nauczanie

Ruy de Queiroz wykładał kilka dyscyplin związanych z logiką i informatyką teoretyczną, w tym teorię mnogości, teorię rekurencji (jako kontynuację kursu prowadzonego przez Solomona Fefermana), logikę dla informatyki, matematykę dyskretną, teorię obliczeń, teorię dowodu , Teoria modeli, Podstawy kryptografii. Miał siedem doktoratów. studentów kierunków Logika Matematyczna i Informatyka Teoretyczna.

Honory i nagrody

Linki zewnętrzne