Equational Reasoning via Maximal Completion

Sarah Winkler - Università di Innsbruck
Data e ora
lunedì 27 maggio 2019 alle ore 15.30 - Sala Riunioni II Piano - Ca' Vignal 2
Referente esterno
Data pubblicazione
13 maggio 2019


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.

© 2002 - 2021  Universit√† degli studi di Verona
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234