А. Смирнов, «Система интерактивного доказательства теорем.», ЛИ, т. 2, сс. 90-104, ноя. 1993.