Eine ausführlich motivierte Einführung von der Aussagenlogik bis zur konstruktiven Typentheorie
Buch, Deutsch, 299 Seiten, Format (B × H): 155 mm x 235 mm
ISBN: 978-3-662-73410-0
Verlag: Springer
Softwareprodukte sind ein integraler Bestandteil unseres alltäglichen Lebens. Die Vielseitigkeit und Komplexität von Software führt aber zu großen Problemen bei ihrer Zuverlässigkeit, insbesondere beim Einsatz in sicherheitskritischen Bereichen. Um wichtige Eigenschaften von Software sicherzustellen, ist es erforderlich, Softwarekomponenten und -systeme mithilfe logisch-formaler Beweissysteme zu verifizieren oder sogar zu synthetisieren.
In diesem Buch werden die theoretischen Grundlagen derartiger Beweissysteme in umfassender Form dargestellt und ausführlich motiviert, so dass sich auch Leser mit geringen Vorkenntnissen einen Überblick über dieses komplexe Gebiet verschaffen können. Es eignet sich als Grundlage für eine entsprechende Lehrveranstaltung, ist aber auch für Spezialisten von Interesse, die sich selbständig in diese Thematik einarbeiten wollen.
Zielgruppe
Upper undergraduate
Autoren/Hrsg.
Fachgebiete
Weitere Infos & Material
1. Einführung.- 2. Formale logische Kalküle.- 3. Der -Kalkül.- 4. Die einfache Typentheorie.- 5. Martin-Löf’s semantische Theorie.- 6. Formale Inferenz in der Typentheorie .- 7. Logik in der Typentheorie.- 8. Programmierung in der Typentheorie.- 9. Fortgeschrittene Konzepte der Typentheorie.- 10. Konstruktion interaktiver Beweisassistenten.- 11. Taktiken – programmierte Beweisführung.- 12. Entscheidungsprozeduren – automatische Beweisführung. 13. Rückblick und Ausblick.
