HP Labs Technical Reports

Linearisation of Omega-Proofs: A New Method of Generalisation within Automated Deduction

Pearson, Siani

HPL-95-93

Keyword(s):

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