Re: Урощение формул

From

Nick Kovaliov ()

To

Vitaly Lugovsky ()

Date

2003-01-25T13:27:31Z

Area

RU.ALGORITHMS

From: "Nick Kovaliov" <Nick@urm.ru>

    VL> Зачем тут нейросети - я так с ходу вряд ли соображу.

Я думаю, что для запоминания "приёмов" доказательств,
и перенесения их на "похожие" ситуации.

    VL> Задача эта - эмпирическая. И NP-полная.
    VL> В известных системах символьной алгебры
    VL> её решают методом правил и стратегий,

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

Стратегий для символьной алгебры ой как много,
и поэтому надо как-то брать стратегии от человека ...

    VL> однако, это явно можно улучшить,
    VL> добавив генетический вывод стратегий.

А может, и не надо от человека брать,
а попробовать генетический вывод.
Полезен он тем, что с течением времени
он будет всё больше приближаться
к оптимальному решению задачи,
а в качестве чего-то начального
можно попробовать взять и человеческое.

    VL> Готовых примеров я не видел, но, думаю,
    VL> для простых случаев реализовать это
    VL> было бы очень даже легко.

Насколько я знаю, такое для
простых примеров делают, и довольно успешно.

Только проблема оказалась даже не в том,
как построить доказательство,
а в том, как сделать результаты
простыми и наглядными для человека.

Попробуй, повозись с простейшими теоремами
внутри теории предикатов (первого порядка) ...
Интуитивно очень просто, а вот попробуй,
построй цепь от начальных аксиом ...
Так вот даже читать готовые цепочки сложно.
Очень сложно выловить понятное ...
Бывает, что строгую формулировку понять сложно,
на это нужна некая особенная тренировка ...

Хотя, может вообще понимание результатов
человеком и не всегда нужно ;-)

До встречи, всего наилучшего !


--- ifmail v.2.15dev5
 * Origin: Demos online service (2:5020/400)