Equational Reasoning via Maximal Completion

Speaker:  Sarah Winkler - Universit√† di Innsbruck
  Monday, May 27, 2019 at 3:30 PM 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):
[1] 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.
[2] S. Winkler. Extending maximal completion. Accepted to Proc. 4th
    FSCD, 2019, to appear.

Programme Director

Publication date
May 13, 2019