Marcela Q. Cruz

On Strong Normalization in Proof-graphs for Propositional Logic

Traditional proof theory of Propositional Logic deals with proofs which size can be huge. Proof theoretical studies discovered exponential gaps between normal or cut free proofs and their respective non-normal proofs. The use of proof-graphs, instead of trees or lists, for representing proofs is getting popular among proof-theoreticians. Proof-graphs serve as a way to provide a better symmetry to the semantics of proofs and a way to study complexity of propositional proofs and to provide more efficient theorem provers, concerning size of propositional proofs. Mimp-graphs was initially developed for minimal implicational logic representing proofs through references rather than copy. Thus, formulas and sub-deductions preserved in the graph structure, can be shared deleting unnecessary sub-deductions resulting in the reduced proof. In this work, we consider full minimal propositional logic and show how to reduce (eliminating maximal formulas) these representations such that strong normalization theorem can be proved by simply counting the number of maximal formulas in the original derivation. In proof-graphs, the main reason for obtaining strong normalization using such simple complexity measure is a direct consequence of the fact that each formula occurs only once in the proof-graph and the case of hidden maximal formula that usually occurs in familiar tree form derivation does representation. A comparison with the proof of strong normalization by means of proving normalization for the worse reduction sequence is discussed.

TecMF: Talks_15_05_15 (last edited 2015-07-15 18:22:35 by HugoMacedo)