Abstrakt. Strukturerade derivat introducerades av Back och von Wright som en förlängning av den beräkningsproof stil som ursprungligen föreslogs av E. W. Dijkstra och hans kollegor. Strukturerade härledningar lade till inbäddade underavdelningar och nedärvda antaganden till denna stil. Genom detta dokument införs ytterligare utvidgningar av det strukturerade härledningsformatet och ger en exakt syntax och semantik för den utökade bevisstilen. Extensions ger en sammanslagning av de tre viktigaste bevis stilar som används i matematik idag: Hilbert-stil framåt kätting proofs, Gentzen-stil bakåt kätting proofs och algebraiska härledning och beräkningar (i synnerhet, Dijkstra beräkningsproof stil). Var och en av dessa bevisstilar kan nu presenteras direkt som en strukturerad härledning. Ännu viktigare, de tre bevis stilar kan fritt blandas i en enda strukturerad härledning, tillåter olika bevis stilar att användas i olika delar av härledningen, varje gång välja den bevisstil som är mest lämplig för (sub) problem till hands. Vi beskriver här (utökad) strukturerad härledning, funktion för funktion, och illustrerar varje funktion med exempel. Vi visar hur man modellerar de tre viktigaste bevisstilarna som strukturerade derivat. Vi ger en exakt syntax för strukturerade derivationer och definierar deras semantik genom att visa hur en strukturerad härledning automatiskt kan översättas till en motsvarande Gentzen-stil sequent calculus härledning. Strukturerade derivat har främst utvecklats för undervisning i matematik på gymnasie- och högskolenivå. Syntaxen för strukturerade härledningar bestämmer bevisets allmänna struktur, men innebär inga begränsningar för hur de grundläggande begreppen i den underliggande matematiska domänen behandlas. Därför kan stilen användas för alla typer av bevis, beräkningar, härledning och allmän problemlösning som finns i matematik utbildning på dessa nivåer. Den exakta syntaxen gör det enkelt att tillhandahålla datorstöd för strukturerade derivat.
I visuellt utseende våra olika bevis stilar, inklusive Coq bevis, liknar de strukturerade derivationer presenteras av Tillbaka i REF.
Structured derivations: a unified proof style for teaching mathematics
{'venue': 'Formal Aspects of Computing', 'journal': 'Formal Aspects of Computing', 'mag_field_of_study': ['Computer Science']}