Linearisation of w-Proofs: ANew Method of Generalisation within Automated Deduction

Abstract. Generalisation is a major 'open ' problem in theorem-proving which must often be addressed when attempting automation of proofs involving mathematical induction. This paper proposes a new, uniform method of generalisation, involving the transformation of proofs, which encompasses many different types of generalisation and which may succeed when other methods fail.