Я нашел подобный вопрос здесь: (5 лет, нет ответа) https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-October/msg00120.html, но это не то же самое.
Давайте предположим, что я доказал классическую теорему как "((А-> В) / \ ((~ А) -> Б)) -> В».Возможно ли в Изабель извлечь термин, подобный одному, на странице 10 этого документа: http://www21.in.tum.de/~berghofe/papers/TYPES2002_slides.pdf.
Я думаю, что важно сделать доказательства независимыми от структуры.Но я также подозреваю, что они не могут быть получены, потому что они не существуют!Например, существует процедура принятия решения, которая может решить, является ли пропозициональная формула тавтологией.Но никакой явный термин не генерируется во время этой процедуры.Являются ли доказательства в Изабель "честными" или "быстрыми" в этом смысле?(Меня особенно интересует Изабель / ZF)