HP Labs Technical Reports
Click here for full text:
Linearisation of Omega-Proofs: A New 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.
Back to Index