{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T10:12:54Z","timestamp":1766139174647,"version":"3.41.0"},"reference-count":23,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.419.4","type":"journal-article","created":{"date-parts":[[2025,5,7]],"date-time":"2025-05-07T11:30:39Z","timestamp":1746617439000},"page":"55-74","source":"Crossref","is-referenced-by-count":2,"title":["OnlineProver: Experience with a Visualisation Tool for Teaching Formal Proofs"],"prefix":"10.4204","volume":"419","author":[{"given":"J\u00e1n","family":"Perh\u00e1\u010d","sequence":"first","affiliation":[{"name":"Technical University of Ko\u0161ice, Slovakia"}]},{"given":"Samuel","family":"Novotn\u00fd","sequence":"additional","affiliation":[{"name":"Technical University of Ko\u0161ice, Slovakia"}]},{"given":"Sergej","family":"Chodarev","sequence":"additional","affiliation":[{"name":"Technical University of Ko\u0161ice, Slovakia"}]},{"given":"Joachim Tilsted","family":"Kristensen","sequence":"additional","affiliation":[{"name":"University of Oslo, Norway"}]},{"given":"Lars","family":"Tveito","sequence":"additional","affiliation":[{"name":"University of Oslo, Norway"}]},{"given":"Oleks","family":"Shturmov","sequence":"additional","affiliation":[{"name":"University of Oslo, Norway, University of Copenhagen, Denmark"}]},{"given":"Michael Kirkedal","family":"Thomsen","sequence":"additional","affiliation":[{"name":"University of Oslo, Norway, University of Copenhagen, Denmark"}]}],"member":"2720","published-online":{"date-parts":[[2025,5,25]]},"reference":[{"key":"baniassadEtal2021","series-title":"SIGCSE '21","doi-asserted-by":"publisher","first-page":"1062","DOI":"10.1145\/3408877.3432430","article-title":"STOP THE (AUTOGRADER) INSANITY: Regression Penalties to Deter Autograder Overreliance","volume-title":"Proceedings of the 52nd ACM Technical Symposium on Computer Science Education","author":"Baniassad","year":"2021"},{"issue":"4","key":"broda2007","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1093\/jigpal\/jzm020","article-title":"Pandora: A Reasoning Toolbox using Natural Deduction Style","volume":"15","author":"Broda","year":"2007","journal-title":"Logic Journal of the IGPL"},{"key":"brooke1996sus","article-title":"SUS: A quick and dirty usability scale","author":"Brooke","year":"1996","journal-title":"Usability Evaluation in Industry"},{"issue":"0","key":"deebHickey2023","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1080\/08993408.2023.2262877","article-title":"Impact of reflection in auto-graders: an empirical study of novice coders","volume":"0","author":"Deeb","year":"2023","journal-title":"Computer Science Education"},{"key":"edwards2004","series-title":"SIGCSE '04","doi-asserted-by":"publisher","DOI":"10.1145\/971300.971312","article-title":"Using software testing to move students from trial-and-error to reflection-in-action","volume-title":"Proceedings of the 35th SIGCSE Technical Symposium on Computer Science Education","author":"Edwards","year":"2004"},{"key":"ehle2018","series-title":"Electronic Proceedings in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.4204\/EPTCS.267.2","article-title":"The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs","volume-title":"Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017","volume":"267","author":"Ehle","year":"2018"},{"key":"frank2018","series-title":"Electronic Proceedings in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.4204\/EPTCS.267.4","article-title":"A Theorem Prover for Scientific and Educational Purposes","volume-title":"Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017","volume":"267","author":"Frank","year":"2018"},{"key":"gasquetEtal2011panda","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-21350-2_11","article-title":"Panda: A Proof Assistant in Natural Deduction for All. A Gentzen Style Proof Assistant for Undergraduate Students","volume-title":"Tools for Teaching Logic","author":"Gasquet","year":"2011"},{"volume-title":"The Logic Manual","year":"2010","author":"Halbach","key":"halbach:2010"},{"article-title":"Deduction using the ProofWeb system","year":"2008","author":"Kaliszyk","key":"kaliszyk2008deduction"},{"issue":"3","key":"karavirtaEtal2006","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1080\/08993400600912426","article-title":"On the use of resubmissions in automatic assessment systems","volume":"16","author":"Karavirta","year":"2006","journal-title":"Computer Science Education"},{"key":"korkut2023","series-title":"Electronic Proceedings in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.4204\/EPTCS.375.5","article-title":"A Proof Tree Builder for Sequent Calculus and Hoare Logic","volume-title":"Proceedings 11th International Workshop on Theorem Proving Components for Educational Software, Haifa, Israel, 11 August 2022","volume":"375","author":"Korkut","year":"2023"},{"key":"KristensenEtal:2024","doi-asserted-by":"publisher","DOI":"10.5324\/nikt.6205","article-title":"OnlineProver: First Experience with Teaching Formal Proofs","volume-title":"UDIT (The Norwegian Conference on Didactics in IT education)","author":"Kristensen","year":"2024"},{"key":"leach-krouse2018","series-title":"Electronic Proceedings in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.4204\/EPTCS.267.5","article-title":"Carnap: An Open Framework for Formal Reasoning in the Browser","volume-title":"Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017","volume":"267","author":"Leach-Krouse","year":"2018"},{"issue":"7","key":"lewis2018","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1080\/10447318.2018.1455307","article-title":"The System Usability Scale: Past, Present, and Future","volume":"34","author":"Lewis","year":"2018","journal-title":"International Journal of Human\u2013Computer Interaction"},{"key":"machin2011yoda","article-title":"Yoda: a simple tool for natural deduction","volume-title":"Proceedings of the Third International Congress on Tools for Teaching Logic (TICTTL\u201911)","volume":"6680","author":"Mach\u00edn","year":"2011"},{"key":"morgan","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-29628-9_1","article-title":"(In-)Formal Methods: The Lost Art","volume-title":"Engineering Trustworthy Software Systems","author":"Morgan","year":"2016"},{"issue":"6","key":"newsome2023mathematical","doi-asserted-by":"publisher","first-page":"1010","DOI":"10.1093\/jigpal\/jzac057","article-title":"What is mathematical logic? An Australian odyssey","volume":"31","author":"Newsome Crossley","year":"2023","journal-title":"Logic Journal of the IGPL"},{"issue":"1","key":"sherin2001","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1011434026437","article-title":"A Comparison of Programming Languages and Algebraic Notation as Expressive Languages for Physics","volume":"6","author":"Sherin","year":"2001","journal-title":"International Journal of Computers for Mathematical Learning"},{"key":"virsedaEtal2011","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-21350-2_29","article-title":"A Logic Teaching Tool Based on Tableaux for Verification and Debugging of Algorithms","volume-title":"Tools for Teaching Logic","author":"del Vado V\u00edrseda","year":"2011"},{"key":"vasconcelos2023","series-title":"Electronic Proceedings in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.4204\/EPTCS.375.4","article-title":"ANITA: Analytic Tableau Proof Assistant","volume-title":"Proceedings 11th International Workshop on Theorem Proving Components for Educational Software, Haifa, Israel, 11 August 2022","volume":"375","author":"Vasconcelos","year":"2023"},{"key":"weintropWilensky2015","series-title":"IDC '15","doi-asserted-by":"publisher","DOI":"10.1145\/2771839.2771860","article-title":"To block or not to block, that is the question: students' perceptions of blocks-based programming","volume-title":"Proceedings of the 14th International Conference on Interaction Design and Children","author":"Weintrop","year":"2015"},{"key":"zenker2011","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-21350-2_30","article-title":"Designing an Introductory Course to Elementary Symbolic Logic within the Blackboard E-learning Environment","volume-title":"Tools for Teaching Logic","author":"Zenker","year":"2011"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2025,5,25]],"date-time":"2025-05-25T09:59:22Z","timestamp":1748167162000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/2505.05987v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,25]]},"references-count":23,"URL":"https:\/\/doi.org\/10.4204\/eptcs.419.4","relation":{},"ISSN":["2075-2180"],"issn-type":[{"type":"electronic","value":"2075-2180"}],"subject":[],"published":{"date-parts":[[2025,5,25]]}}}