Herbelin presented at CSL'94 a simple sequent calculus for minimal implicational logic, with a complete set of cut-reduction rules which is both confluent and strongly normalising. We describe briefly its utility for proof search and its relationship to calculi for uniform proof search; our novel point is that if one adds cut-reduction rules to allow simulation of ordinary beta-reduction one has a system which is still confluent and strongly normalising, and in fact preserves strong normalisability of untyped terms, thus solving a problem left open by Herbelin. We speculate about the possibility of extending the calculus to allow confluence on open terms ("meta-confluence") but retaining the SN-property.

This is joint work with Christian Urban, Cambridge.