Если есть способ реализовать профиле для математической индукции, как бы это выглядело? Если это невозможно, почему?Автоматическая проверка теорем для математической индукции
Я подумал о том, как указать основные аксиомы и правила в качестве ввода и ограничить его проблемами с основными суммами и уравнениями.
Будет ли это так же, как и для математических доказательств?
Я буду держать ответ ограниченным индукцией по натуральным числам.
Позвольте S(n) быть заявлением, которое вы хотите подтвердить по индукции для всех n. Затем программе необходимо будет проверить: S(0) и S(n) => S(n+1).
Первая часть так же сложна, как и доказательство некоторого утверждения, вторая часть доказывает эквивалентность двух таких утверждений. Это означает, что даже если первая часть не является трудной, вторая часть может быть NP-hard (к моему knowlegde). Так что да, может быть реализован proofer (просто нужно проверить одно утверждение и эквивалентность двух операторов), но я не думаю, что вы можете гарантировать его прекращение.
BTW, не все доказательства начинаются с S (0). Во многих случаях вы начинаете с константы, а затем принимаете для n, а затем доказываете для n + 1. –
@GoodLuck вы можете сделать каждое доказательство, начиная с постоянного начала с 0 – WorldSEnder
Под «proofer» вы имеете в виду алгоритм, который находит доказательство для данного утверждения? Тьюринг показал, что это невозможно сделать в целом. Если вы имеете в виду машину, которая выводит доказательства на основе данных аксиом, это возможно. Но индукция является такой важной частью теории аксиоматических чисел, что почти все доказательства используют индукцию на той или иной стадии. –