Здравствуйте, pagid, Вы писали:
vsb>>Смысл хотя бы в том, чтобы проверка и принятие доказательств новых теорем занимала миллисекунды, а не годы, как это иногда бывает. P>А не пришлось бы для действительно новых теорем каждый раз прикручивать новые расширения к языку? Отлаживать и тестировать машину вывода, видимо на примере этой самой новой теоремы
