[Club2] Einladung: Techniques for First-Order Term Indexing in Isabelle/ML - Mi 28. Apr. 2021 14:00 - 14:30 (MESZ) (club2 at mailbroy.informatik.tu-muenchen.de)
piller at in.tum.de
piller at in.tum.de
Mon Apr 26 10:44:15 CEST 2021
Sie wurden zum folgenden Termin eingeladen.
Titel: Techniques for First-Order Term Indexing in Isabelle/ML
Speaker: Sebastian WillenbrinkType: Bachelor's Thesis Presentation
Abstract: In recentyears, increasingly powerful proof automation has been
introduced tointeractive theorem provers such as Isabelle. This automation
necessitatesefficient datastructures to index and query sets of terms.
So-called termindices provide queries for retrieving variants, instances,
generalisations andunifiables of a given term. Two indexing techniques,
path indexing anddiscrimination tree indexing are reviewed. We implement
path indexing forfirst-order terms in Isabelle/ML and adapt it to the more
general term indexinginterface defined in Isabelle/ML. We further define a
unified interface for thepath index and the previously implemented
discrimination tree index, therebyclearing the way for the implementation
of additional term indices in thefuture. Lastly, we evaluate the
performance of path indexing in relation todiscrimination tree indexing.
Wann: Mi 28. Apr. 2021 14:00 – 14:30 Mitteleuropäische Zeit - Berlin
Wo: https://tinyurl.com/ls21coffee
Kalender: club2 at mailbroy.informatik.tu-muenchen.de
Wer
* piller at in.tum.de- Veranstalter
* club2 at mailbroy.informatik.tu-muenchen.de
* sebastian.willenbrink at tum.de
Termininformationen:
https://calendar.google.com/calendar/event?action=VIEW&eid=M2hwcWZwcXI1ZWE4dWhlYmNmYXYya3RtaGMgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTkzYWNmYzg1N2MxY2JjNjIyYTM1YjBiYzg4NDA0MGJjYjI4NTg1ZmE&ctz=Europe%2FBerlin&hl=de&es=0
Einladung von Google Kalender: https://calendar.google.com/calendar/
Sie erhalten diese E-Mail unter club2 at mailbroy.informatik.tu-muenchen.de,
da Sie ein Gast bei diesem Termin sind.
Lehnen Sie diesen Termin ab, um keine weiteren Informationen zu diesem
Termin zu erhalten. Sie können auch unter
https://calendar.google.com/calendar/ ein Google-Konto erstellen und Ihre
Benachrichtigungseinstellungen für Ihren gesamten Kalender steuern.
Wenn Sie diese Einladung weiterleiten, kann jeder Empfänger eine Antwort an
den Organisator senden und zur Gästeliste hinzugefügt werden. Außerdem
könnte er weitere Nutzer einladen und Ihre Antwort ändern. Weitere
Informationen: https://support.google.com/calendar/answer/37135#forwarding
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210426/3efd27f9/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2600 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210426/3efd27f9/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 2650 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210426/3efd27f9/attachment.bin>
More information about the Club2
mailing list