Abstrakt. Vi introducerar och studerar ett taktikspråk, Hitac, för att konstruera hierarkiska bevis, så kallade hiproofs. Tanken med hiproofs är att lägga ett märkt hierarkiskt bo på ett vanligt bevisträd. Etiketterna och häckningen används för att beskriva organisationen av beviset, vanligtvis i samband med dess konstruktionsprocess. Detta kan vara användbart för att förstå och navigera bevis. Taktik i vårt språk konstruerar hiproof struktur tillsammans med ett underliggande bevisträd. Vi erbjuder både ett stort steg och en liten steg operativ semantik för att utvärdera taktikuttryck. De stora steg semantik fångar den avsedda betydelsen, medan de små steg semantik pekar på möjliga implementationer och ger en enhetlig uppfattning om bevistillstånd. Vi bevisar att dessa begrepp är likvärdiga och konstruerar giltiga bevis.
Aspinall m.fl. REF introducerar taktikspråket Hitac som kan användas för att konstruera hierarkiska bevis, så kallade hiproofs.
A Tactic Language for Hiproofs
{'venue': 'AISC/MKM/Calculemus', 'journal': None, 'mag_field_of_study': ['Computer Science']}