Поисковик для теорем

h_alishov

Известны ли поисковики по теоремам? Хочется иметь функциональность наподобие: известно, что среди того, что дано есть оператор с точечным спектром, хочется доказать, что его обратный оператор компактен. Требуется найти теоремы, которые связаны с данным утверждением. Например, кроме точечного спектра еще что-то, в итоге получаем желаемое.
А то сейчас ботаю, а поскольку мне навскидку помнятся далеко не все теоремы в функане, довольно много времени тратится на поиск нужной теоремы.

zzzXAXAXAzzz

Известны ли поисковики по теоремам?

Мне не известны, но ты четко расписал, что они должны делать, примерно, я так предполагаю, даже представляешь функциональную модель, тем более с ВМиК... Вот она - отличная программа для написания, все будут благодарны.

lenmas

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

h_alishov

Гуглом сейчас и пользуюсь. Все равно теряется времени больше, чем хочется. Причем, в разы больше.

h_alishov

Вот она - отличная программа для написания, все будут благодарны
Сама по себе программа-то простая, но забивка теорем — работа объемная, нудная и при этом требующая хороших знаний в каждой области математики. Т.е. это недешевая задача, одному человеку поднять тяжело, а много людей без денег работать не умеют практически.

Zoltan

нужно что-то википодобное

h_alishov

В общем-то хочется что-то типа этого, только более широкого, с умным (см. выше) поиском по теоремам (по определениям и по содержанию есть).
зы. Стоимость создания упомянутого проекта оценивается в 100-200 килобаксов, т.к. в нем уже более 12000 статей, каждая из которых снабжена ссылками на литературу, примерами и пр. Очевидно, что создание подобной вещи с нуля и на энтузиазме — задача малореальная.
Пока что склоняюсь к тому, чтобы просто прикрутить к этому ресурсу "внешний" поиск. Правда, неясно, что делать с теми теоремами, которые остались за бортом этого ресурса. Лично мне нужны пусть и в достаточно узкой теме, но как можно больше теорем и формулировок одной и той же теоремы (с разными условиями и результатами).

chepa02

что-то такое?
The Encyclopaedia of Mathematics is a large reference work in mathematics. It is available in book form, on CD-ROM, and can also be browsed online for free. The 2002 version contains more than 8,000 entries covering most areas of mathematics at a graduate level, and the presentation is technical in nature. The encyclopedia is edited by Michiel Hazewinkel and was published by Kluwer Academic Publishers until 2003, when Kluwer became part of Springer. The CDROM contains animations and three-dimensional objects.
The encyclopedia has been translated from the Soviet Matematicheskaya entsiklopediya (1977) originally edited by Ivan Matveevich Vinogradov and extended with comments and three suplements adding several thousand articles.

здесь онлайн вариант, неудобный совершенно:
http://eom.springer.de/default.htm
диск с глобальным полнотекстовым поиском и гипертекстом стоит 1900 баксов

h_alishov

да. Что-то такое. Только хочется, чтобы были учтены достижения математики хотя бы года до 1995-го и теоремы не до уровня "graduate" (такие я более-менее наизусть помню а порядка "postdoc" (или как там пишется)

h_alishov

хм. Ща посмотрел — а вполне достойный сайт. Лучше, чем про него говорит описание. Спасибо за ссылку.
правда, все равно для моих потребностей мало

chepa02

советская энциклопедия - это как раз не студенческий уровень, вот только с последними достижениями не знаю как у них, описаны ли

h_alishov

увы, нет. Да и с малоизвестными теоремами проблемы. Боюсь по причине огромного количества теорем в мире такой проект пока еще не сделан.
Прям хоть щас беги и заявку на грант в РФФИ или такого рода фонды оформляй.

chepa02

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

h_alishov

результаты у них уже какие-то есть? как-нибудь узнать это возможно через кого-нибудь?

chepa02

не знаю, насколько я поняла - у них все-таки первым делом объединение библиотек в единую сеть было
тут где-то надо искать, точнее не помню уже
www.emis.de

h_alishov

Спасибо, сейчас посмотрю, что у них есть.

h_alishov

Ае! Нашелся таки поисковик примерно такой, который и хотелось. клац. Правда, работает только у тех, у кого открыт порт 58081, и синтаксис какой-то очень странный, но это уже почти то, что хочет партия.
upd. Все настолько странное, что даже интерпретировать результаты поиска тестового примера мне не удалось. Предлагается ввести \forall n:nat.n \lt n+5, нажать на кнопочку hint и получить подсказку, как доказать, что n < n+5. Выводится ответ:
1. cic:/Coq/Arith/Plus/lt_plus_trans.con
ObjectВ lt_plus_trans:
В В В

2. cic:/Rocq/THREE_GAP/Nat_compl/lt_plus.con
ObjectВ lt_plus:
В В В

3. cic:/Coq/Arith/Lt/lt_S_n.con
ObjectВ lt_S_n:
В В В

4. cic:/CoRN/ftc/COrdLemmas/om_fun_lt.con
ObjectВ om_fun_lt:
В В В

5. cic:/Coq/Arith/Plus/plus_lt_reg_l.con
ObjectВ plus_lt_reg_l:
В В В [ Loading ... please wait ]

6. cic:/Cachan/SMC/misc/lt_trans_1.con
ObjectВ lt_trans_1:
В В В [ Loading ... please wait ]

7. cic:/Coq/Arith/Lt/lt_trans.con
ObjectВ lt_trans:
В В В [ Loading ... please wait ]

8. cic:/Nijmegen/QArith/sqrt2/monotonic_inverse.con
ObjectВ monotonic_inverse:
В В В [ Loading ... please wait ]

Идейно поисковик мб и неплох, но он явно только для орков.
upd2 Поиск теорем/определений там похоже сломался и давно.

stm7535571

Да, unibo давно уже скорее мёртв чем жив. Да и база там от CoQ, так что теорем не много, хотя зато все теоремы проверенные.
Из многообещающих проектов лучше смотреть что-нибудь вроде http://planetmath.org, но там тоже пока дальше университетского курса не пошло. Хотя определения чёткие в большинстве своём.

h_alishov

спасибо за ссылку, заценил. Судя по всему, это как раз пример проекта, который организован а-ля wiki и тянется исключительно на энтузиазме. Посмотрим, что у них получится, но в современном виде, к сожалению, пользы мало.
Оставить комментарий
Имя или ник:
Комментарий: