ИСТИНА

Отчет по проекту РФФИ. Работа посвящена созданию методов поиска информации для структурированных файлов. Рассматривается формат musicXML. В качестве поискового запроса задается фрагмент нотной записи и ставится задача поиска нот произведения, содержащего данный фрагмент (в том числе записанный в другой тональности, для другого инструмента). Метод поиска основывается на методах автоматических рассуждений. При поиске возникает задача сравнения похожих фрагментов. Подобная задача решается при построении доказательства методом математической индукции, когда рассматриваются гипотеза и заключение индукции, которые также являются похожими.Для автоматизации доказательства методом индукции используются волновые правила (rippling), цель которых - устранить различия в похожих выражениях. Правила построены на основе аксиом предметной области и на каждом шаге их применения количество различий уменьшается. В работе метод применен к задаче поиска нот: на основе музыкальной теории построены волновые правила, позволяющие проводить сравнение нотных фрагментов, оценивать их похожесть. В работе также проанализировано применение метода для файлов, содержащих формулы формата mathML. Входными данными для поиска является математическая формула, результатом - набор документов, содержащих запись похожих формул.