HP Labs Technical Reports

Click here for full text: PDF

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

Pearson, Siani



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

[Research] [News] [Tech Reports] [Palo Alto] [Bristol] [Japan] [Israel] [Site Map] [Home] [Hewlett-Packard]