Strong cut-elimination in sequent calculus using Klop's iota-translation and perpetual reductions.

Morten Heine Sørensen Pawel Urzyczyn

Published in: J. Symb. Log. (2008)

Keyphrases

sequent calculus
cut elimination
inference rules
linear logic
natural deduction
modal logic
wide class
linear time temporal logic
first order logic
sufficient conditions
high level
fixed point
theorem prover
theorem proving
logical framework
proof search