A human-oriented term rewriting system

Add to your list(s) Download to your calendar using vCal

• Ed Ayers (University of Cambridge)
• Monday 23 September 2019, 13:00-14:00
• FC22.

If you have a question about this talk, please contact Mateja Jamnik.

I will give a talk on a paper I have written with Mateja Jamnik and Tim Gowers , which I will be presenting at KI in Germany this week.

We introduce a fully automatic system, implemented in the Lean theorem prover, that solves equality problems of everyday mathe- matics. Our overriding priority in devising the system is that it should construct proofs 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, the program finds a promising subtask, such as rewriting a subterm, and places 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.

This talk is part of the Artificial Intelligence Research Group Talks (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Artificial Intelligence Research Group Talks (Computer Laboratory)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge Forum of Science and Humanities
• Cambridge Language Sciences
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• FC22
• Guy Emerson's list
• Hanchen DaDaDash
• Interested Talks
• School of Technology
• Speech Seminars
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• rp587
• yk373's list

Note that ex-directory lists are not shown.