Dragoon
Удален
|
    
Пишу роботу по обратному методу. Вопросов больше, чем ответов в найденнной литературе. Сейчас прочитал некоторые роботы С.Ю. Маслова, А.Воронкова ("The Inverse Method"), читаю роботу Ф.Пфенинга ("Automated Theorem Prooving"). Очень хотел бы, чтобы отозвался кто-то, кто также читал и разобрался в этих работах.
В роботе Пфенинга непонятно следующее:
В чем суть оптимизационных техник инверсности (inversing) и фокусирования (focusing)?
Кроме того, хотелось бы узнать, чем отличаются классическая логика и интуиционистская? Из того, что я слышал - тем, что в интуиционистской логике отсутствует правило исключенного третьего. Хотелось бы знать точно.
Могу ли я работать с равенством через механизм унификации - а именно проводить преобразования подобно:
P(a,x,y)&x=z or not P(z,a,f(x))
=>
(P(a,a,a) or not P(a,a,f(a)))*{z/x,a/z,f(x)/y}
?
|
Форум
Секвенциальное исчисление, обратный метод
