Interactive Proof Assistant Based on Floyd-Hoare Logic
Samuel Novotný, William Steingartner, Katarína Sivá, Ján Perháč · 2025
This paper focuses on the development of an in-teractive proof assistant for visualizing the axiomatic semantics of a simple imperative language, specifically proofs in Hoare logic. The goal is to provide students with an easily accessible interactive environment where they can independently explore this semantic method, with the option of receiving feedback. The form of a web application offers the required easy access, independent of the platform, and the continuously evolving web development frameworks provide numerous components that ensure a simple, interactive, and functional user interface, which is essential for the comfortable use of this tool and, ultimately, a better understanding of this subiect.