Monday, May 27, 2019
Sala Riunioni II Piano - Ca' Vignal 2
Maximal completion is a simple yet powerful approach to Knuth-Bendix completion based on maxSMT. The talk first describes how this method extends to ordered completion and gives rise to a competitive equa- tional theorem prover. In the next step the approach is integrated into an instantiation-based theorem proving loop. Maximal completion itself as well as instantiation-based theorem proving can be seen as conflict-driven procedures. The talk focuses on the underlying deduction systems as implemented in the equational theorem prover maedmax, but also discusses certification of tool results as well as machine learning as a means to improve heuristics.
References (to some of the content, if required):  S. Winkler and G. Moser. Maedmax: A maximal ordered completion tool. In Proc. 9th IJCAR, volume 10900 of LNCS, pages 472–480, 2018. doi: 10.1007/978-3-319-94205-6_31.  S. Winkler. Extending maximal completion. Accepted to Proc. 4th FSCD, 2019, to appear. http://cl-informatik.uibk.ac.at/users/swinkler/research/papers/W-FSCD19.pdf