BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A human-oriented term rewriting system - Ed Ayers (University of C
 ambridge)
DTSTART:20190923T120000Z
DTEND:20190923T130000Z
UID:TALK131437@talks.cam.ac.uk
CONTACT:Mateja Jamnik
DESCRIPTION:I will give a talk on a paper I have written with Mateja Jamni
 k and Tim Gowers \, which I will be presenting at KI in Germany this week.
 \n\nWe introduce a fully automatic system\, implemented in the Lean theore
 m prover\, that solves equality problems of everyday mathe- matics. Our ov
 erriding priority in devising the system is that it should construct proof
 s of equality in a way that is similar to that of humans. A second goal is
  that the methods it uses should be domain independent. The basic strategy
  of the system is to operate with a subtask stack: when- ever there is no 
 clear way of making progress towards the task at the top of the stack\, th
 e program finds a promising subtask\, such as rewriting a subterm\, and pl
 aces that at the top of the stack instead. Heuristics guide the choice of 
 promising subtasks and the rewriting process. This makes proofs more human
 -like by breaking the problem into tasks in the way that a human would. We
  show that our system can prove equality theorems simply\, without having 
 to preselect or orient rewrite rules as in standard theorem provers\, and 
 without having to invoke heavy duty tools for performing simple reasoning.
LOCATION:FC22
END:VEVENT
END:VCALENDAR