У статті представлено схему зворотного методу для обчислення висловлювань, що може працювати з формулами, представленими у вигляді секвенцій загального вигляду, викладені доповнення до конструктивного алгоритму зворотного методу, а також наведена схема механізму іменування для можливості здійснення скороченого виведення.
