В работе рассматриваются вопросы создания интерфейсов с ЭВМ. Представлено описание экспериментальной системы для решения задач, сводимых к доказательству теорем. Система поддерживает ввод информации на языках разного уровня - от ограниченного естественного языка до языка многосортного исчисления предикатов первого порядка. В качестве тестовых для разработки системы были выбраны задачи из евклидовой геометрии на плоскости. Поиск вывода осуществляется методом синтаксического дерева.
Система содержит подсистемы доказательства теорем, поддержки базы знаний, пояснения решения и общения на ограниченном естественном языке, включающую блок ведения словаря, позволяющий пополнять словарь в ходе работы системы.
Cистема реализована на метаязыке Рефал. Предложенные средства, в свою очередь, можно рассматривать как определенное расширение метаязыка для построения трансляторов широкого класса с использованием созданных библиотек функций. К их числу относятся функции для пополнения базы знаний, логического вывода и для синтаксического анализа предложений. Средства синтаксического анализа можно рассматривать как дополнительные метаязыковые средства для построения синтаксически управляемого контекстного макрогенератора.
