Рюи де Кейрос

Рюи де Кейрос

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

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

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

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

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

исследовал С начала 2000-х годов Рюи де Кейроз совместно с Анжолиной де Оливейра геометрическую перспективу естественной дедукции, основанную на графическом описании симметричной естественной дедукции Нила .

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

• Член консультативной группы Комитета премии имени Рольфа Шока в области логики и философии (2008 и 2011 гг.) (Шведская королевская академия наук);
• Главный редактор Логического журнала Группы по интересам в области чистой и прикладной логики , Oxford University Press, 1993 – настоящее время;
• Заместитель редактора журнала Computer System and Sciences , координатор и соучредитель (совместно с Д. Габбаем) Группы по интересам в области чистой и прикладной логики (IGPL), информационно-координационного центра Европейской ассоциации логики, языка и информации (FoLLI), 1990 – настоящее время;
• Приглашенный редактор нескольких томов (в сотрудничестве с несколькими всемирно известными логиками и учеными-компьютерщиками, такими как Джон Болдуин, Сергей Н. Артемов , Бруно Пуаза, Декстер Козен, Ангус Макинтайр, Григори Минтс, Уилфрид Ходжес, Анудж Давар, Хироакира Оно, Макото Канзава, Даниэль Лейвант, Лев Беклемишев) «Анналов чистой и прикладной логики», «Теоретическая информатика, информация и вычисления», «Журнал компьютерных систем и наук», «Фундамента информатика», несколько томов «Электронных заметок по теоретической информатике»;
• Создатель и главный организатор серии семинаров 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. Паб., Дордрехт, июль 2003 г., ISBN   1-4020-1270-5 , стр. 3–88.
4. Смысл, функция, цель, полезность, последствия – понятия взаимосвязанные. Логический журнал группы по интересам в области чистой и прикладной логики, 9 (5): 693-734, сентябрь 2001 г., Oxford Univ. Нажимать.
5. (совместно с Габбаем, Д.) Маркированный естественный вычет. В логике, языке и рассуждении. Очерки в честь Дова Габая, Х. Дж. Ольбаха и У. Рейла (ред.), том 5 серии «Тенденции в логике», Kluwer Academic Publishers, Дордрехт, июнь 1999 г., стр. 173–250.
6. (совместно с де Оливейрой, А.) Процедура нормализации для эквационального фрагмента помеченного естественного вывода. Логический журнал группы по интересам в области чистой и прикладной логики, 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 '91, Уппсала. Аннотация в JSL 58(2):753-754, 1993.
8. Нормализация и языковые игры. In Dialectica 48(2):83-123, 1994. (Ранняя версия представлена ​​на Logic Colloquium '88, Падуя. Аннотация в JSL 55:425, 1990.)
9. (совместно с Габбаем, Д.) Распространение интерпретации Карри-Ховарда на линейную, релевантную и другие ресурсные логики, в Journal of Символическая логика 57 (4): 1319-1365. Доклад, представленный на коллоквиуме Logic '90, Хельсинки. Аннотация в JSL 56(3):1139-1140, 1991.
10. (совместно с Майбаумом, Т.) Абстрактные типы данных и теория типов: теории как типы, в журнале Mathematical Logic and Foundations of Mathematics 37:149-166.
11. (совместно с Майбаумом Т.) Теория доказательств и компьютерное программирование, в журнале математической логики и основах математики 36: 389-414.
12. Теоретико-доказательное описание программирования и роли правил редукции, в Dialectica 42(4):265-282.
13. де Кейроз, Р. де Оливейра, А., и Габбай, Д.: 2011, Функциональная интерпретация логической дедукции. Том. 5 из серии «Прогресс в логике». Издательство Имперского колледжа / World Scientific. ISBN   978-981-4360-95-1 .

Обучение

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

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

• Приглашенный профессор Тинкера в Стэнфордском университете , присуждаемый The Tinker Foundation по номинации Соломона Фефермана и Григория Минца , 2005 г.;
• Стипендия для иностранных студентов-исследователей, Комитет проректоров и директоров Лондонского университета , 1985–1987 годы.

Внешние ссылки

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