Semantisches Browsen
Aus International Center for Computational Logic
'''This course is offered for the "Komplex … '''This course is offered for the "Komplexpraktikum Wissensbasierte Systeme".'''</br></br>This course aims to give a practical introduction to the LEAN interactive theorem prover. To this end, students are asked to formalize various definitions and results from the "Formale Systeme" undergraduate lecture in LEAN. After an introductory session, a weekly option for consultation will be offered. The individual results are presented in a colloquium at the end of the semester.</br></br>In the previous semester, a group of students made the first step towards having "Formale Systeme" formalized in LEAN. We are collecting the results of this course in our [https://github.com/knowsys/Formale-Systeme-in-LEAN GitHub repository]. Of course, the current state of the formalization and the results may be used and extended throughout this course's procedure.</br></br>Additional information and updates will be communicated through the respective matrix channel.ted through the respective matrix channel. +
Referat +
Lecturer
Lecturers
Lukas Gerlach; Stephan Mennicke +
Module
INF-B-510, INF-B-520, INF-MA-PR +
* https://leanprover.github.io/
* https:/ … </br>* https://leanprover.github.io/</br>* https://adam.math.hhu.de/</br>* https://leanprover-community.github.io/mathlib_docs/</br>* Moura, L.d., Ullrich, S. (2021). The Lean 4 Theorem Prover and Programming Language. In: Platzer, A., Sutcliffe, G. (eds) Automated Deduction – CADE 28. CADE 2021. Lecture Notes in Computer Science https://leanprover.github.io/papers/lean4.pdf</br>tps://leanprover.github.io/papers/lean4.pdf
+
0 +
0 +
Anzeigetitel„Anzeigetitel <span style="font-size:small;">(Display title of)</span>“ ist ein softwareseitig fest definiertes Attribut, das einen eindeutigen Anzeigetitel zu einem Objekt speichert und ihm zuweist. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
Theorem Proving with LEAN +
Zuletzt geändert„Zuletzt geändert <span style="font-size:small;">(Modification date)</span>“ ist ein softwareseitig fest definiertes Attribut, das das Datum der letzten Änderung einer Seite speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
15. November 2023, 13:02:06 +
Hat Abfrage„Hat Abfrage <span style="font-size:small;">(Has query)</span>“ ist ein softwareseitig fest definiertes Attribut, das die Metainformationen einer Abfrage als <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Subobject">Subobjekt</a> speichert. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
Hat Unterobjekt„Hat Unterobjekt <span style="font-size:small;">(Has subobject)</span>“ ist ein softwareseitig fest definiertes Attribut und stellt einen <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Container">Datenverbund</a> dar. Es wird von <a rel="nofollow" class="external text" href="https://www.semantic-mediawiki.org/wiki/Help:Special_properties">Semantic MediaWiki</a> zur Verfügung gestellt.
