ИСТИНА

Работа посвящена созданию новых методов информационного поиска для специализированных предметных областей. В настоящее время существует огромное количество разного рода информации, хранящейся в электронном виде, и для работы с ней нужны СУБД и поисковые системы. Несмотря на наличие современных поисковых систем, успешно решающих свою задачу, все еще остаются области, не охваченные ими. Такой является задачи поиска нот музыкальных произведений по заданному фрагменту мелодий и поиск текстов, в которых встречается заданное математическое выражение. Несмотря на то, что области разные, данные для поиска в них обеих хранятся в формате, основанном на XML: это формат MusicXML для нот и MathML для формул, то есть задача поиска ставится для структурированных документов. При поиске релевантными имеет смысл считать не только документы, содержащие в себе данные из поискового запроса: мелодия может быть той же, но записанной в другой тональности (и, следовательно, у нее будет другое символьное преставление), формула может совпадать с искомой с точностью до имен переменных или же может быть приведена к искомой применением известных математических тождеств. Для поиска с учетом этих особенностей предлагается использовать методы автоматического доказательства теорем, в частности волновые правила (rippling). Метод волновых правил применяется в доказательстве по индукции, когда гипотеза и заключение являются синтаксически похожими, размечаются их различия и делается попытка их устранить с помощью специальных правил переписывания – волновых правил. Такие правила не затрагивают общие фрагменты выражений, а с каждым шагом их применения должно уменьшаться количество различий, поэтому процесс применения правил завершается. При применении метода в данных областях необходимо составить набор подходящих правил, определить меру, для оценки количества различий. В работе планируется адаптация метода автоматических рассуждений с помощью волновых правил (rippling) для решения задачи информационного поиска.