Semantic programming and polynomially computable representations

In the present article, we consider the question on existence of polynomially computable representations for basic syntactic constructions of the first-order logic and for objects of semantic programming (such as L-programs and L-formulas). We prove that the sets of linear or tree-like derivations in the first-order predicate calculus admits a polynomially computable representation. We also obtain a series of assertions that allow us to prove polynomial computability in a more efficient way. Among them, we mention the generalized PAG-theorem with polynomially computable initial data and an assertion on p-iterative terms with weakened estimates. Our results may be useful for construction of logical programming languages, in smart contracts, as well as for developing fast algorithms for automatic proof verification.