Рюи де Кейруш - Ruy de Queiroz

Ruy de Queiroz bw

Руй Дж. Герра Б. де Кейруш (родился 11 января 1958 г. в г. Ресифи ) является адъюнкт-профессором Федерального университета Пернамбуку и проводит важные работы в области исследований математической логики, теории доказательств, основ математики и философии математики.[1] Он является основателем Практикум по логике, языку, информации и вычислениям (WoLLIC), который проводится ежегодно с 1994 года, обычно в июне или июле.

Руи де Кейруш получил степень бакалавра в области электротехники в Escola Politecnica de Pernambuco в 1980 году, степень магистра информатики в Федеральный университет Пернамбуку в 1984 г. и его докторскую степень в области вычислительной техники Имперский колледж, Лондон в 1990 г., защитил диссертацию. Теория доказательств и компьютерное программирование. Очерк логических основ вычислений.

Профиль исследования

В конце 1980-х Рюи де Кейруш предложил новую формулировку Теория типа Мартина-Лёфа основанный на прочтении романа Витгенштейн «Значение-есть-использование», где объяснение последствий данного предложения придает смысл логической константе, доминирующей в предложении. Это равносильно недиалогической интерпретации логических констант через эффект правил исключения над правилами введения, что находит параллель в Пол Лоренцен 'песок Яакко Хинтикка диалог / игра-семантика. Это привело к появлению теории типов под названием «Смысл как теория типов использования».[2] В отношении использования изречения Витгенштейна он показал, что аспект, касающийся объяснения последствий предложения, присутствует с очень ранней даты, когда в письме к Бертран Рассел, где Витгенштейн ссылается на универсальный квантор, имеющий значение только тогда, когда человек видит то, что из него следует.[3]

Позднее, в 1990-х, Рюи де Кейруш был помолвлен вместе с Дов Габбай, в программе предоставления общего описания функциональной интерпретации классической и неклассической логики через понятие помеченного естественного вывода. В результате были предложены новые объяснения функциональной интерпретации квантора существования, а также понятие пропозиционального равенства, последнее позволяло пересмотреть Ричард Статман понятие прямого вычисления, а также новый подход к дихотомии «интенсиональный и экстенсиональный» учет пропозиционального равенства через Переписка Карри – Ховарда.

С начала 2000-х годов Руи де Кейруш ведет расследование совместно с Анжолина де Оливейра, геометрическая перспектива естественного вывода, основанная на графическом учете Kneale Симметричный естественный вывод.[4]

Служение профессии

  • Член консультативной группы комитета по присуждению премии Рольфа Шока в области логики и философии (2008 и 2011 гг.) (Шведская королевская академия наук);
  • Главный редактор журнала Logic Journal of the Interest Group in Pure and Applied Logics, Oxford University Press, 1993 - по настоящее время;
  • Заместитель редактора Journal of Computer System and Sciences, координатор и соучредитель (вместе с Д. Габбаем), Interest Group in Pure and Applied Logics (IGPL), расчетной палаты Европейской ассоциации логики, языка и информации (FoLLI) 1990 – настоящее время;
  • Приглашенный редактор нескольких томов (в сотрудничестве с несколькими всемирно известными логиками и компьютерными учеными, такими как Джон Болдуин, Сергей Н. Артемов, Bruno Poizat, Dexter Kozen, Angus Macintyre, Grigori Mints, Wilfrid Hodges, Anuj Dawar, Hiroakira Ono, Makoto Kanzawa, Daniel Leivant, Lev Beklemishev) из Анналов чистой и прикладной логики, теоретической информатики, информации и вычислений, Journal of Computer System and Sciences, Fundamenta Informaticae, несколько томов электронных заметок по теоретической информатике;
  • Создатель и главный организатор серии мастер-классов WoLLIC (http://www.cin.ufpe.br/~wollic );
  • Член редакционного совета Международного справочника логиков, Д. Габбей и Дж. Вудс (ред.), College Publications;
  • Избранный член Совета Ассоциации символической логики, 2006–2008 годы.

Ключевые публикации

  1. (совместно с де Оливейрой А.) Функциональная интерпретация прямых вычислений. Электронные заметки по теоретической информатике 269: 19-40, 2011.
  2. О правилах редукции, значении как использовании и теоретико-доказательной семантике, Studia Logica 90 (2): 211-247, ноябрь 2008 г.
  3. (совместно с де Оливейрой, А.) Геометрия вывода через графы доказательства. В «Логике для параллелизма и синхронизации» Р. де Кейро (ред.), Том 18 серии «Тенденции в логике», Kluwer Acad. Pub., Дордрехт, июль 2003 г., ISBN  1-4020-1270-5С. 3–88.
  4. Значение, функция, цель, полезность, последствия - понятия взаимосвязанные. Logic Journal of the Interest Group in Pure and Applied Logics, 9 (5): 693-734, сентябрь 2001 г., Oxford Univ. Нажмите.
  5. (совместно с Габбаем, Д.) Обозначенное естественное удержание. В логике, языке и рассуждениях. Очерки в честь Дов Габбая, Х. Дж. Ольбаха и У. Рейла (редакторы), том 5 серии «Тенденции в логике», издательство Kluwer Academic Publishers, Дордрехт, июнь 1999 г., стр. 173–250.
  6. (совместно с де Оливейрой, А.) Процедура нормализации для фрагмента уравнения помеченного естественного выведения. Logic Journal of the Interest Group in Pure and Applied Logics, 7 (2): 173-215, 1999, Oxford Univ. Нажмите. Полная версия статьи представлена ​​на 2-й конференции WoLLIC'95, Ресифи, Бразилия, июль 1995 г. Реферат опубликован в Journal of the Interest Group in Pure and Applied Logics 4 (2): 330-332, 1996.
  7. (совместно с Габбаем, Д.) Функциональная интерпретация экзистенциального квантификатора, в Bulletin of the Interest Group in Pure and Applied Logics 3 (2-3): 243-290, 1995. (Специальный выпуск по дедукции и языку, приглашенный редактор: Рут Кемпсон). Полная версия доклада представлена ​​на Logic Colloquium '91, Уппсала. Резюме в JSL 58 (2): 753-754, 1993.
  8. Нормализация и языковые игры. In Dialectica 48 (2): 83-123, 1994. (Ранняя версия представлена ​​на Logic Colloquium '88, Padova. Резюме в JSL 55: 425, 1990.)
  9. (с Габбаем, Д.) Расширение интерпретации Карри-Ховарда на линейные, релевантные и другие логики ресурсов, в Journal of Symbolic Logic 57 (4): 1319-1365. Доклад представлен на Logic Colloquium '90, Хельсинки. Резюме в JSL 56 (3): 1139-1140, 1991.
  10. (совместно с Майбаумом Т.) Абстрактные типы данных и теория типов: теории как типы, в Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 37: 149-166.
  11. (совместно с Майбаумом Т.) Теория доказательства и компьютерное программирование, в Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 36: 389-414.
  12. Теоретико-доказательственное рассмотрение программирования и роли правил редукции, в Dialectica 42 (4): 265-282.
  13. de Queiroz, R. de Oliveira, A., & Gabbay, D .: 2011, Функциональная интерпретация логического вывода. Vol. 5 из серии достижений в логике. Imperial College Press / World Scientific. ISBN  978-981-4360-95-1.

Обучение

Рюи де Кейруш преподавал несколько дисциплин, связанных с логикой и теоретической информатикой, включая теорию множеств, теорию рекурсии (как продолжение курса Соломона Фефермана), логику для компьютерных наук, дискретную математику, теорию вычислений, теорию доказательств. , Теория моделей, Основы криптографии. Он имеет семь кандидатов наук. студенты в области математической логики и теоретической информатики.

Почести и награды

Рекомендации

  1. ^ ГАББАЙ, Дов М .; ВУДС, Джон (27 апреля 2009 г.). Международный справочник логиков. Публикации колледжа. ISBN  978-1-904987-90-1. Получено 2011-07-28.
  2. ^ де Кейруш, Р. «Смысл как грамматика плюс последствия», в Диалектика 45(1):83-86.
  3. ^ де Кейро, Р. «Математический язык и его семантика: показать следствия предложения - значит дать его значение». В Вайнгартнер, Пауль и Шурц, Герхард, редакторы, Доклады Тринадцатого Международного симпозиума Витгенштейна 1988 г., том 18 Schriftenreihe der Wittgenstein-Gesellschaft, Вена, 304 стр. Гёльдер – Пихлер – Темпски, стр. 259–266. Симпозиум проходил в Кирхберге / Векселе, Австрия, 14–21 августа 1988 г.
  4. ^ де Кейруш; де Оливейра (2011). «Пропозициональное равенство, типы идентичности и прямые вычислительные пути». arXiv:1107.1901 [cs.LO ].

внешняя ссылка