Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Ruy de Queiroz bw

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

Руи де Кейруш получил B.Eng в электротехнике эскола Politecnica де Пернамбуку в 1980 году, его M.Sc по информатике с Федеральным университетом де Пернамбуку в 1984 году, и его доктор философии в области вычислительной техники из Imperial College , Лондон в 1990 году, для которой он защитил диссертацию по теории доказательства и компьютерному программированию. Очерк логических основ вычислений .

Профиль исследования [ править ]

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

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

С начала 2000-х Руи де Кейруш совместно с Анжолиной де Оливейра исследовал геометрическую перспективу естественного вывода, основанную на графическом описании симметричного естественного вывода Книла. [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 – настоящее время;
  • Приглашенный редактор нескольких томов (в сотрудничестве с несколькими авторитетными логиками и компьютерными учеными, такими как Джон Болдуин, Сергей Н. Артемов , Бруно Пойза, Декстер Козен, Ангус Макинтайр, Григорий Минц, Уилфрид Ходжес, Анудж Давар, Хироакира Оно, Макото Канзава, Даниэль Лейвант, Лев Беклемишев) из «Анналов чистой и прикладной логики, теоретической информатики, информации и вычислений», журнала «Компьютерные системы и науки», «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., Dordrecht, июль 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. (совместно с Габбаем, Д.) Функциональная интерпретация экзистенциального квантификатора, Бюллетень группы интересов по чистой и прикладной логике 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. де Кейруш, Р. де Оливейра, А., и Габбей, Д.: 2011, Функциональная интерпретация логической дедукции. Vol. 5 из серии достижений в логике. Imperial College Press / World Scientific. ISBN 978-981-4360-95-1 . 

Обучение [ править ]

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

Почести и награды [ править ]

Ссылки [ править ]

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

Внешние ссылки [ править ]

  • Домашняя страница профессионального профиля Рюя Герры