Документы РС-формы можно преобразовать в формат DOC (MS Word) для дальнейшего распространения, включения в другие документы, печати. Чтобы экспортировать документ РС-формы КС необходимо использовать пункт меню Файл / Экспорт. Окно экспорта представлено на Рис. 1.
При экспорте необходимо выбрать нотацию, в которой записываются имена и формальные выражения конституент. Существуют две распространенные в области ТЛКП нотации ЯРС. Стандартная нотация, разработанная А. В. Ключниковым и В. А. Тищенко, использована в программном комплексе Экстеор и в работах А. В. Майорова и А. Д. Грязнова над программой "DBTeor". Классическая нотация, разработанная Д. Б. Персицем, использована в работе И. Н. Пономарева над программным продуктом "Бурбакизатор". Результаты сравнения двух нотаций представлены в Табл. 1. Символом # отображается номер конституенты, задаваемый набором арабских цифр.
В Экстеор 4 исторически используется стандартная нотация. Тем не менее при экспорте документа РС-формы в текстовый формат пользователю предоставляется выбор между нотациями.
Название | Стандарт | Классика (по Тищенко) |
Базисное множество | X# | X# |
Константное множество | C# | C# |
Родовая структура | S# | D# |
Ступень | H# | S# |
Аксиома | A# | Ax# |
Терм | D# | Tr# |
Терм-функция | F# | TF# |
Теорема | T# | Th# |