New proof simplifies weak normalization for propositional logic
Simplified proofs of Weak Normalization for propositional logic
Logic in Computer Science
Summary
Logic proofs can sometimes get complicated, especially when trying to simplify or 'normalize' them. The authors found an easier way to show that any proof in a certain style of logic can be simplified. They do this by focusing on entire parts of the proof, rather than breaking them into smaller segments. They also created clear rules and a step-by-step method for this simplification, and showed it works by programming it in a computer language called Lean.
What this means in practice
- •For formal verification engineers: Implement clear procedures for proof simplification in automated reasoning tools to improve verification confidence.
- •For programming language designers: Design programming languages or proof assistants that use deterministic algorithms for normalizing proofs to optimize proof checking and compilation.
A theory result. No direct application yet.
Authors
S P Suresh
Abstract
We present a new proof of weak normalization for intuitionistic natural deduction. The distinguishing features of this proof are that it works only with cuts rather than cut segments, provides explicit local rules for determining whether to contract a whole proof or reduce one of its subproofs, and in the latter case, which subproof to reduce. We also discuss a formalization of the entire proof in Lean, and present a deterministic algorithm for weak normalization.