Reduction of Hilbert-type proof systems to the if-then-else equational logic (Q1428985)

The notion of \(p\)-simulation [see \textit{S. Cook} and \textit{R. Reckhow}, J. Symb. Log. 44, 36--50 (1979; Zbl 0408.03044)] gives a tool to measure the relative efficiency of various proof systems. In this paper the author generalizes this notion and presents a construction of the linear reduction of Hilbert-type proof systems of propositional logics to if-then-else equational logic. The construction presented is strong enough to linearly reduce first-order logic to if-then-else equational logic as well.