В 1973-м году вышла книжка
1973, Chin-Liang Chang & Richard Char-Tung Lee, Symbolic Logic & Mechanical Theorem Proving

в 1983-м году её перевели на русский язык
1983, Ч. Чень & Р. Ли, Математическая логика и автоматическое доказательство теорем

Я хотел бы узнать, у кого насколько глубокое понимание всей этой области? Особенно у БудДена. С одной стороны он лиспер, значит должен в этом всём разбираться. С другой стороны, он неуважительно высказывался по поводу доказуемости ядра L4 (что говорит о том, что он в деталях с этой системой доказывания не разобрался).

Моя проблема заключается в том, что я тоже не разобрался.
В частности я не понимаю перехода между логическим выводом и разбором предложений в алгоритме FCG.

Отредактировано Лис (2020-02-27 21:48:11)