Руи Дж. Герра Б. де Кейрос (родился 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 годы.
Ключевые публикации [ править ]
- (совместно с де Оливейрой, А.) Функциональная интерпретация прямых вычислений. Электронные заметки по теоретической информатике 269: 19-40, 2011.
- О правилах редукции, значении как использовании и теоретико-доказательной семантике, Studia Logica 90 (2): 211-247, ноябрь 2008 г.
- (совместно с де Оливейрой, А.) Геометрия вывода через графы доказательства. В «Логике для параллелизма и синхронизации» Р. де Кейро (ред.), Том 18 серии «Тенденции в логике», Kluwer Acad. Pub., Dordrecht, июль 2003 г., ISBN 1-4020-1270-5 , стр. 3–88.
- Значение, функция, цель, полезность, последствия - понятия взаимосвязанные. Logic Journal of the Interest Group in Pure and Applied Logics, 9 (5): 693-734, сентябрь 2001 г., Oxford Univ. Нажмите.
- (совместно с Габбаем, Д.) Обозначенная естественная дедукция. В логике, языке и рассуждениях. Очерки Дова Габбая, Х. Дж. Ольбаха и У. Рейла (редакторы), том 5 серии «Тенденции в логике», издательство Kluwer Academic Publishers, Дордрехт, июнь 1999 г., стр. 173–250.
- (совместно с де Оливейрой, А.) Процедура нормализации для фрагмента уравнения помеченного естественного выведения. 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.
- (совместно с Габбаем, Д.) Функциональная интерпретация экзистенциального квантификатора, Бюллетень группы интересов по чистой и прикладной логике 3 (2-3): 243-290, 1995. (Специальный выпуск по дедукции и языку, приглашенный редактор: Рут Кемпсон). Полная версия доклада представлена на Logic Colloquium '91, Уппсала. Резюме в JSL 58 (2): 753-754, 1993.
- Нормализация и языковые игры. In Dialectica 48 (2): 83-123, 1994. (Ранняя версия представлена на Logic Colloquium '88, Padova. Резюме в JSL 55: 425, 1990.)
- (с Габбаем, Д.) Расширение интерпретации Карри-Ховарда на линейные, релевантные и другие логики ресурсов, в Journal of Symbolic Logic 57 (4): 1319-1365. Доклад представлен на Logic Colloquium '90, Хельсинки. Резюме в JSL 56 (3): 1139-1140, 1991.
- (совместно с Майбаумом Т.) Абстрактные типы данных и теория типов: теории как типы, в Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 37: 149-166.
- (совместно с Майбаумом Т.) Теория доказательства и компьютерное программирование, в Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 36: 389-414.
- Теоретико-доказательство программирования и роли правил редукции, в Dialectica 42 (4): 265-282.
- де Кейруш, Р. де Оливейра, А., и Габбей, Д.: 2011, Функциональная интерпретация логической дедукции. Vol. 5 из серии достижений в логике. Imperial College Press / World Scientific. ISBN 978-981-4360-95-1 .
Обучение [ править ]
Руи де Кейруш преподавал несколько дисциплин, связанных с логикой и теоретической информатикой, включая теорию множеств, теорию рекурсии (как продолжение курса Соломона Фефермана), логику для компьютерных наук, дискретную математику, теорию вычислений, теорию доказательств. , Теория моделей, Основы криптографии. Он имеет семь кандидатов наук. студенты в области математической логики и теоретической информатики.
Почести и награды [ править ]
- Приглашенная профессура Тинкер в Стэнфордском университете , присужденная Фондом Тинкер после номинации, данной Соломоном Феферманом и Григорием Минцем , 2005;
- Стипендия для иностранных студентов-исследователей, Комитет проректоров и директоров Лондонского университета , 1985–1987 годы.
Ссылки [ править ]
- ^ ГАББЕЙ, Дов М .; ЛЕС, Джон (27 апреля 2009 г.). Международный справочник логиков . Публикации колледжа. ISBN 978-1-904987-90-1. Проверено 28 июля 2011 .
- ^ de Queiroz, R. «Смысл как грамматика плюс последствия», в Dialectica 45 (1): 83-86.
- ^ de Queiroz, R. «Математический язык и его семантика: показать следствия предложения - значит дать его значение». В Вайнгартнер, Пауль и Шурц, Герхард, редакторы, Отчеты Тринадцатого Международного симпозиума Витгенштейна 1988 г. , том 18 Schriftenreihe der Wittgenstein-Gesellschaft, Вена, 304 стр. Гёльдер – Пихлер – Темпски, стр. 259–266. Симпозиум проходил в Кирхберге / Векселе, Австрия, 14–21 августа 1988 г.
- ^ де Кейруш; де Оливейра (2011). «Пропозициональное равенство, типы идентичности и прямые вычислительные пути». arXiv : 1107.1901 [ cs.LO ].
Внешние ссылки [ править ]
- Домашняя страница профессионального профиля Рюя Герры