Post production system

Post normal system, Post normal calculus

A particular case of a Post canonical system when all derivation rules have the form

$$\frac{Gp}{pG}$$

and there is only one initial word (one axiom of the considered calculus). E. Post [1] has established the equivalence in the wide sense between Post production systems and Post canonical systems. Post production systems were used by Post and A.A. Markov (1947) to construct the first examples of an associative calculus with an unsolvable word problem (Thue's problem).

References

[1]	E.L. Post, "Formal reductions of the general combinatorial decision problem" Amer. J. Math. , 65 : 2 (1943) pp. 197–215
[2]	A.A. Markov, "Theory of algorithms" , Israel Program Sci. Transl. (1961) (Translated from Russian) (Also: Trudy Mat. Inst. Steklov. 42 (1954))

References

[a1]	H.B. Curry, "Foundations of mathematical logic" , McGraw-Hill (1963)