статьи Е. Орловской "Automatic theorem proving in a certain class of formulae of predicate calculus".
