Semantic Programming and Polynomially Computable Representations
Andrey Vitalievich Nechesov · Siberian Advances in Mathematics · 2023
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.