- Seminari
- Equational Reasoning via Maximal Completion
Equational Reasoning via Maximal Completion
Relatore
Sarah Winkler - Università di Innsbruck
Data
27-mag-2019 - Ora:
15:30
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.
http://cl-informatik.uibk.ac.at/users/swinkler/research/papers/W-FSCD19.pdf
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.
http://cl-informatik.uibk.ac.at/users/swinkler/research/papers/W-FSCD19.pdf
- Data pubblicazione
- 13-mag-2019
- Dipartimento
- Informatica
