Folke: En bevisredigerare för naturlig deduktion

Abstract

Denna rapport introducerar Folke, en bevisredigerare för naturlig deduktion för förs ta ordningens logik. Logik tillhandahåller ett ramverk för formellt resonerande där man konstruerar nya påståenden utifrån initiala påståenden som kallas premisser. Ett bevis är en korrekt formulerad sekvens av påståenden som utifrån givna pre misser når en önskad slutsats. Folke var utformad för att hjälpa studenter i logik att formulera och verifiera sina bevis. Tidigare mjukvarulösningar har en tendens att vara svåranvända och ointuitiva för nybörjare på grund av deras komplexitet. För att bemöta detta har Folke utvecklats med fokus på användarvänlighet, med ett interaktivt och nybörjarvänligt gränssnitt med tydliga felmeddelanden. Programmet har implementerats i Haskell, och användargränssnittet har byggts med hjälp av det komponentbaserade GUI-biblioteket Monomer. Folke distribueras som ett program tillgängligt för Linux, Windows och Mac OS. Framtida förbättringar kan inkludera ett hjälpsystem för bevissteg, förbättrad tolkning för mer informativa felmedde landen samt en användarstudie för att vägleda fortsatt utveckling och identifiera eventuella buggar.