  We present a~novel approach to the problem of automated theorem proving.
Polynomial cost procedures that recognise sentences belonging to a theory are
generated on a basis of a set of axioms of the so-called Truncated Predicate
Calculus being a~subset of standard predicate calculus. Several exemplary
problems are included to show the performance of the proposed approach.
