{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T05:17:07Z","timestamp":1751606227585,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,15]],"date-time":"2020-06-15T00:00:00Z","timestamp":1592179200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Linz Institute of Technology","award":["LOGTECHEDU"],"award-info":[{"award-number":["LOGTECHEDU"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,15]]},"DOI":"10.1145\/3341525.3387409","type":"proceedings-article","created":{"date-parts":[[2020,6,3]],"date-time":"2020-06-03T04:15:40Z","timestamp":1591157740000},"page":"61-67","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App"],"prefix":"10.1145","author":[{"given":"David","family":"Cerna","sequence":"first","affiliation":[{"name":"Johannes Kepler University, Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[{"name":"Johannes Kepler University, Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Schreiner","sequence":"additional","affiliation":[{"name":"Johannes Kepler University, Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Windsteiger","sequence":"additional","affiliation":[{"name":"Johannes Kepler University, Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[{"name":"Johannes Kepler University, Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,6,15]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"James Aczel P. Fung Richard Bornat Martin Oliver Tim O'Shea and Bernard Sufrin. 1999. Using computers to learn logic: undergraduates' experiences. 875--882.  James Aczel P. Fung Richard Bornat Martin Oliver Tim O'Shea and Bernard Sufrin. 1999. Using computers to learn logic: undergraduates' experiences. 875--882."},{"key":"e_1_3_2_1_2_1","volume-title":"2nd","volume":"48","author":"Alves Sandra","year":"2011"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Serge Autexier Christoph Benzm\u00fcller Dominik Dietrich Andreas Meier and Claus-Peter Wirth. 2006. A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity. In Mathematical Knowledge Management Michael Kohlhase (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 126--142.  Serge Autexier Christoph Benzm\u00fcller Dominik Dietrich Andreas Meier and Claus-Peter Wirth. 2006. A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity. In Mathematical Knowledge Management Michael Kohlhase (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 126--142.","DOI":"10.1007\/11618027_9"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Tiffany Barnes and John Stamper. 2008. Toward Automatic Hint Generation for Logic Proof Tutoring Using Historical Student Data. In Intelligent Tutoring Systems Beverley P. Woolf Esma A\u00efmeur Roger Nkambou and Susanne Lajoie (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 373--382.  Tiffany Barnes and John Stamper. 2008. Toward Automatic Hint Generation for Logic Proof Tutoring Using Historical Student Data. In Intelligent Tutoring Systems Beverley P. Woolf Esma A\u00efmeur Roger Nkambou and Susanne Lajoie (Eds.). Springer Berlin Heidelberg Berlin Heidelberg 373--382.","DOI":"10.1007\/978-3-540-69132-7_41"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Mordechai Ben-Ari. 2012. Mathematical Logic for Computer Science 3rd ed.). Springer London.  Mordechai Ben-Ari. 2012. Mathematical Logic for Computer Science 3rd ed.). Springer London.","DOI":"10.1007\/978-1-4471-4129-7"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74565-5_34"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9072-3"},{"volume-title":"Proceedings of the 6th Int. Workshop on Theorem Proving components for Educational software, ThEdu@CADE'17","year":"2017","author":"B\u00f6hne Sebastian","key":"e_1_3_2_1_8_1"},{"key":"e_1_3_2_1_9_1","first-page":"3","article-title":"Animating Formal Proof at the Surface","volume":"42","author":"Bornat R.","year":"1999","journal-title":"The Jape Proof Calculator. Comput. J."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Joachim Breitner. 2016. Visual Theorem Proving with the Incredible Proof Machine. In Interactive Theorem Proving Jasmin Christian Blanchette and Stephan Merz (Eds.). Springer International Publishing Cham 123--139.  Joachim Breitner. 2016. Visual Theorem Proving with the Incredible Proof Machine. In Interactive Theorem Proving Jasmin Christian Blanchette and Stephan Merz (Eds.). Springer International Publishing Cham 123--139.","DOI":"10.1007\/978-3-319-43144-4_8"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzm020"},{"volume-title":"Natural Deduction: A Proof-Theoretical Study","year":"1965","author":"Prawitz Dag","key":"e_1_3_2_1_12_1"},{"volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning, Christian G","author":"Preining Norbert","key":"e_1_3_2_1_13_1"},{"key":"e_1_3_2_1_14_1","unstructured":"Steve Reeves and Michael Clarke. 1990. Logic for Computer Science .Addison-Wesley Boston MA USA.  Steve Reeves and Michael Clarke. 1990. Logic for Computer Science .Addison-Wesley Boston MA USA."},{"key":"e_1_3_2_1_15_1","unstructured":"Stuart J. Russell and Peter Norvig. 2010. Artificial Intelligence - A Modern Approach Third Int. Edition .Pearson Education Upper Saddle River NJ USA.  Stuart J. Russell and Peter Norvig. 2010. Artificial Intelligence - A Modern Approach Third Int. Edition .Pearson Education Upper Saddle River NJ USA."},{"key":"e_1_3_2_1_16_1","volume-title":"Pedro Quaresma and Walther Neuper (Eds.)","volume":"290","author":"Schreiner Wolfgang","year":"2019"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2674683.2674696"},{"key":"e_1_3_2_1_18_1","unstructured":"Terry Tao. 2018. QED. (2018). https:\/\/teorth.github.io\/QED\/  Terry Tao. 2018. QED. (2018). https:\/\/teorth.github.io\/QED\/"},{"key":"e_1_3_2_1_19_1","unstructured":"Laurent Th\u00e9ry. [n. d.]. Peanoware-Natural Deduction. Google Play. ([n. d.]).  Laurent Th\u00e9ry. [n. d.]. Peanoware-Natural Deduction. Google Play. ([n. d.])."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"J\u00f8rgen Villadsen Andreas Halkj\u00e6r From and Anders Schlichtkrull. 2019. Natural Deduction Assistant (NaDeA). In rm Proceedings 7th International Workshop on Theorem proving components for Educational software rm Oxford United Kingdom 18 july 2018 (Electronic Proceedings in Theoretical Computer Science) Pedro Quaresma and Walther Neuper (Eds.) Vol. 290. Open Publishing Association 14--29. https:\/\/doi.org\/10.4204\/EPTCS.290.2  J\u00f8rgen Villadsen Andreas Halkj\u00e6r From and Anders Schlichtkrull. 2019. Natural Deduction Assistant (NaDeA). In rm Proceedings 7th International Workshop on Theorem proving components for Educational software rm Oxford United Kingdom 18 july 2018 (Electronic Proceedings in Theoretical Computer Science) Pedro Quaresma and Walther Neuper (Eds.) Vol. 290. Open Publishing Association 14--29. https:\/\/doi.org\/10.4204\/EPTCS.290.2","DOI":"10.4204\/EPTCS.290.2"},{"key":"e_1_3_2_1_21_1","unstructured":"Yale Weiss. 2016. LOGIC+. (2016). https:\/\/yaleweiss.commons.gc.cuny.edu\/logic\/  Yale Weiss. 2016. LOGIC+. (2016). https:\/\/yaleweiss.commons.gc.cuny.edu\/logic\/"}],"event":{"name":"ITiCSE '20: Innovation and Technology in Computer Science Education","sponsor":["SIGCSE ACM Special Interest Group on Computer Science Education"],"location":"Trondheim Norway","acronym":"ITiCSE '20"},"container-title":["Proceedings of the 2020 ACM Conference on Innovation and Technology in Computer Science Education"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341525.3387409","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341525.3387409","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:12:58Z","timestamp":1750201978000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341525.3387409"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,15]]},"references-count":21,"alternative-id":["10.1145\/3341525.3387409","10.1145\/3341525"],"URL":"https:\/\/doi.org\/10.1145\/3341525.3387409","relation":{},"subject":[],"published":{"date-parts":[[2020,6,15]]},"assertion":[{"value":"2020-06-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}