Алгоритм поиска вывода в чистом логическом каркасе

Аннотация

Чистый логический каркас - это такой логический каркас, который не базируется на каком-либо
конкретном формальном исчислении. Например, Metamath (http://metamath.org) является образцом
чистого логического каркаса. Другим примером является система Russell (https://github.com/dmitry-vlasov/russell-flow),
которая может считаться языком более высокого уровня по отношению к Metamath. В данной статье описан
алгоритм поиска доказательств, применяющийся в Russell. Доказано, что алгоритм корректен и полон, то есть
он порождает правильные доказательства и любое правильное доказательство (с точностью до подстановки) может быть
найдено этим алгоритмом.