Edward William Ayers: Human-like automated reasoning

Datum objave: 19. 11. 2018
Seminar za temelje matematike in teoretično računalništvo
Četrtek, 22. 11. 2018, od 11h do 13h, učilnica 3.07, Jadranska 21

Abstract: In this talk I will give a summary of my research in to human-like automated reasoning. Which I define as proving theorems on a computer in a way that reflects some aspect of how a human would approach proving them. I present a new approach for term rewriting developed in conjunction with Tim Gowers and Mateja Jamnik that can solve simple term rewriting problems using ‘subgoals’ which are stacks of intermediate tasks concerning the syntax of the terms that must be shown to be equal.

I will also discuss the earlier work of Tim Gowers and Mohan Ganesalingam that serves as the foundation for this approach.