Жак Эрбран: логика, которая стала языком программирования

Жак Эрбран был французским математиком, чья карьера оборвалась трагически рано. Он погиб в 1931 году в возрасте 23 лет, взбираясь на гору в Альпах. Но за свою короткую жизнь он совершил открытие, которое изменило компьютерные науки.
Момент прорыва:
В своей диссертации 1930 года Эрбран доказал фундаментальную теорему: любое утверждение логики первого порядка можно свести к проверке истинности конечного числа propositional формул (формул без кванторов).
Проще говоря: если у вас есть сложное утверждение с кванторами ∀ и ∃, теорема Эрбрана говорит, как превратить его в огромную (но конечную) логическую задачу, которую можно решить механически.
Наследие:
В 1970-х годах на основе идей Эрбрана был создан язык программирования Prolog (Programming in Logic). В Prolog вы не пишете алгоритм — вы описываете факты и правила, а система сама ищет решение, используя метод резолюций Эрбрана.
«Логика — это не просто инструмент мышления. Это язык, на котором можно программировать». Жак Эрбран показал это первым.