Reduction of Hilbert-type proof systems to the if-then-else equational logic (Q1428985)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Reduction of Hilbert-type proof systems to the if-then-else equational logic |
scientific article; zbMATH DE number 2063137
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Reduction of Hilbert-type proof systems to the if-then-else equational logic |
scientific article; zbMATH DE number 2063137 |
Statements
Reduction of Hilbert-type proof systems to the if-then-else equational logic (English)
0 references
29 March 2004
0 references
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.
0 references
Hilbert-type proof system
0 references
equational logic
0 references
relative efficiency of proof systems
0 references
0 references
0 references
