Department of Computer Science and Technology

Technical reports

A new application for explanation-based generalisation within automated deduction

Siani L. Baker

February 1994, 18 pages

DOIhttps://doi.org/10.48456/tr-327

Abstract

Generalisation is currently a major theorem-proving problem. This paper proposes a new method of generalisation, involving the use of explanation-based generalisation within a new domain, which may succeed when other methods fail. The method has been implemented for simple arithmetical examples.

Full text

PDF (1.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-327,
  author =	 {Baker, Siani L.},
  title = 	 {{A new application for explanation-based generalisation
         	   within automated deduction}},
  year = 	 1994,
  month = 	 feb,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-327.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-327},
  number = 	 {UCAM-CL-TR-327}
}