How can we better reduce barriers to learning for ADHD students whilst encouraging the development of critical thinking in the age of Generative AI?
Backlinks
AI Disclosure
I was one of the student testers for Microsoft Copilot ahead of its wider rollout to all students. The tests that influenced this assignment included: breaking down the assignment brief into a checklist and questions, which helped the drafting process; searching online for additional sources to fill perceived gaps in my existing choice of sources (which contributed less than 5% of my original collection of 221 sources); and identifying sources I had saved to my OneDrive that I forgot to move to my references folder.
Separately to these student tests, I also used Microsoft Copilot to learn new programming languages and troubleshoot code, which influenced decision-making; develop and refine example problem scenarios in Prolog, Rocq and Isabelle/HOL, as well as AI system prompts, for preliminary testing of my ideas; and create BibLaTeX citations for sources.
Additionally, due to my preference for direct experimentation after reading and accidentally collecting an unreasonably large number of sources, I used Copilot to assist in prioritising and organising the sources. I created an Excel spreadsheet including all the sources and questions I either felt were relevant or had influenced my thinking towards this assignment and had Copilot extract quotes based on these, adding summaries to preserve context. I reviewed these, manually corrected some quotes using the original sources, categorised sources and identified which sources to exclude.
I then used Copilot as a drafting tool, instructing it not to provide any new ideas except for my own and from the quotes, as well as instructing Copilot to analyse and apply my writing style from a previous assignment. After this, I manually refined the entirety of the draft and manually checked citations again to ensure the interpretations and ideas provided were appropriately attributed, as well as trying to get closer to the word limit.
After finalising this part of the assessment and in preparation for the part 2 evaluation video, I provided GPT 6 Astra with this written assessment to see if it could create a more functional prototype followed by a few iterations of feedback. Originally, I planned to assess Gemma 4 and Isabelle/HOL as separate tools to argue for feasibility but, based on GPT 6 Astra’s output, I decided to instead evaluate the prototype.
1 Problem Statement
The challenge we focus on is to provide a digital resource catered to ADHD students who wish to develop their argumentation skills across disciplines. To truly cater to this audience, we must understand the different aspects of ADHD and the wider context.
As a late-diagnosed ADHD student, I wish to explore how digital technologies could be used to reduce barriers relating to attention and executive dysfunction, so that I can have an alternative means of engaging in active learning that better meet my needs. I’ve found that existing reasonable adjustments are inadequate in meeting my needs, and this is a recognised problem in ADHD literature that requires urgent action by universities (Green and Rabiner, 2012, Mestichelli et al., 2026).
I’m also a part-time PhD student in Pure Maths and, when engaging with my previous PGCert assignment, I found that the process of synthesising and refining a critical analysis essay was similar to constructing mathematical proofs. Through my research for this project, I discovered that this overlap was recognised as “argumentation” (Almpani, Stefaneas and Vandoulakis, 2023).
Through understanding my needs, I learnt that:
- Reduction in ADHD-related difficulties is associated with increased external demands and norepinephrine levels (Killeen, 2019, Sibley et al., 2024);
- ADHDers have an increased need for appropriate delivery speed of information (Martella et al., 2020);
- Forced breaks have a detrimental impact on ADHD productivity (X. Xu et al., 2025).
Through personal exploration, recreational stress activities can indirectly help task initiation, but it is unreliable and can itself become a distraction. More broadly, stress responses are individual and context-dependent (Cavaleri et al., 2023, Córdova et al., 2023, Y. Liu et al., 2025). Thus, a digital tool targeting ADHD students should provide adjustable challenge, optional inclusion of healthy stressors, and enables continuous engagement with variable pace.
As a disability advocate, I’ve observed students experiencing increased pressure from external factors (Finn et al., 2025, Jisc, 2025) and experiencing cognitive fatigue from high course workloads. Disabled students also experience a disproportionate increase in fatigue and stress (Disabled Students Sector Leadership Group, 2017, Horlin et al., 2024, Jones, 2023). This fatigue and stress can impact executive functioning skills similarly to ADHD, which are essential skills when independent learning is required (CAST, no date). Thus, I believe traditional formal approaches to support may act as a barrier in retrieving academic skills support. Additionally, Le Cunff (2024) suggests future research and practice should explore how to nurture curiosity to reduce ADHD barriers to education and, as a Library Student Team Member, we also have a responsibility to ensure our support is interdisciplinary. Hence, the digital tool should use a personalised playful learning approach, which consequently meets multiple Universal Design for Learning considerations (CAST, 2024, Quigley and Gallagher, 2025).
Reflecting on Gabe Newell’s view on piracy and his explanations behind Valve’s approach against it (Gabe says piracy isn’t about price, 2011), I concluded that the general temptation to cheat as being induced by design problems such as the intended experiences being inaccessible, unrewarding, or fail to mitigate extrinsic pressures, including whether cheating is perceived as socially acceptable. This interpretation is supported by video game literature on cheating (Hamlen and Gage, 2011, Han, Kwak and H. K. Kim, 2022, S. J. Lee et al., 2023, Mulakaluri et al., 2024, Passmore et al., 2020, Wu and Chen, 2018) and higher education literature on academic misconduct (Miles, Campbell and Ruxton, 2022, Sozon et al., 2024, 2026, Yusuf, Pervin and Román-González, 2024). Within our context, only 21% of students feel their courses reward thinking and reasoning (Dickinson and Marshall, 2026) and some assessments are returning to timed in-person exams in response to worries about AI misconduct (Robert et al., 2026), which can disadvantage students with ADHD (X. Xu et al., 2025). I decided to focus on Game-based learning (GBL) to explore how gamified assessment-feedback loops could provide insights into how we could continue provision of inclusive assessments that reward the process of reasoning, and because it can also create an authentic context for argumentation (Song and Sparks, 2019b).
Lastly, embedding anticipatory inclusive teaching practices requires adequate resources, time, sustained engagement, and staff support (Disabled Students Sector Leadership Group, 2017). While staff training and resources are needed to develop accessible materials (Finn et al., 2025), there is a need to reduce institutional pressures placed on academics, which contributes to an inability to provide sufficient accommodations to disabled people (Horlin et al., 2024). Digital transformation similarly introduces additional requirements for adequate resources, staff support, and reduced institutional pressures (Mabotha and Ngcamu, 2026, Robert et al., 2025). These pressures disproportionately impact disabled academics too (Horlin et al., 2024, Jones, 2023). Our digital solutions should therefore anticipate insufficient staff capacity by also catering to students as an assistive tool.
2 Project Aim and Objectives
Aim: to develop a personalised game-based argumentation sandbox as an assistive software for ADHD students.
Intended Impacts:
- Students will be better incentivised to engage in their own independent critical thinking more positively.
- Students will be provided with more control over the level of positive sources of stress when engaging in learning.
- Staff will be better supported in making appropriate accommodations for ADHD learners.
- Practitioners will be provided with insights on assessment design practices and their effectiveness in discouraging academic misconduct.
Intended Outcomes:
- Students will be able to apply their argumentation skills across different disciplines and contexts.
- Students will be evaluated on their performance across different scenarios and feedback provided during scenario debrief to make transferable concepts explicit.
- Students will be able to synthesise arguments in their own words based on a set of provided facts with sufficient depth in solving interactive scenarios.
- Students will be evaluated based on whether they solve the interactive scenarios using automated logic verification.
- Students will be able to evaluate and refine their arguments in response to conversation.
- Students will be actively evaluated during the interactive scenarios and receive AI-generated feedback in the form of Socratic Questioning.
- Students and Staff will be able apply their subject knowledge towards creating argumentation problem scenarios using the digital tool with relative ease.
- Students and Staff will be required to self-evaluate but will have the option to share this through feedback forms to ensure the tool is continuously refined.
To determine whether the project is sufficient in meeting the short-term outcomes, we will evaluate whether the outcomes are met during student testing where we can receive participant consent. Project evaluation will only test implementation and early outcome evidence, not causal impact.
Intended Activities:
- Design a backend system that can be locally hosted on edge devices that provides an automated argumentation assessment and feedback loop.
- Develop a minimal and accessible user interface for students and staff to interact with and develop customised argumentation scenarios.
3 Literature Review
The literature suggests that digital interventions should not digitise proof practice directly, but create low-stakes, scaffolded and transparent reasoning practice that supports student agency before, during and after AI-generated feedback (Song and Sparks, 2019b, X. Xu et al., 2025).
When designing learning environments, we should treat barriers as environmental rather than individual (Disabled Students Sector Leadership Group, 2017, Erbil, Özbilgin and Gündoğdu, 2025, Robert et al., 2025). The user interface should therefore prioritise offering multiple routes for engagement, representation, action and expression (CAST, 2024), which also includes enabling verbal explanation as an alternative to typed. This should include adjustable complexity, reduced distractions (Atkinson, Sajka and Wolberger, 2026) and avoid unnecessary context-switching (Center for Humane Technology, no date). These can partially be addressed by ensuring the solution includes onboarding processes and minimal task switching, which are already required in order to avoid assuming the existence of digital natives or that students can multitask effectively with unfamiliar digital tools (Kirschner and De Bruyckere, 2017).
GBL should treat interaction and meaningful feedback as core elements (Tatnall, 2020). As part of its assessment design, it should collect reliable and valid evidence of students’ knowledge and skills (Song and Sparks, 2019a). Evidence-Centred Design requires us to make the evidentiary chain explicit by connecting argumentation constructs, observable performances that evidence skill, and the activities designed to demonstrate these (DiCerbo, 2017, Song and Sparks, 2019b) and formally verified argumentation meets these, however expecting students to formalise their evolving arguments may reduce engagement (Almpani, Gkantzounis and Stefaneas, 2026).
Perháč, Suliman and Novotný (2026) and Zibrowius (2026) provide examples of interactive games that show playful proof practice is possible. However, they are not appropriate solutions for our problem as they are limited to mathematical argumentation and focus learning on the formalised proof languages. Therefore, our solution should instead focus on providing the natural language to formal verification loop, which GenAI is capable of doing (Agarwal et al., 2026, Bringsjord et al., 2024, Pei, Du and Jin, 2025, Yang et al., 2025).
Since we intend to formally verify argumentation, the user interface may benefit from the same features as Interactive Theorem Provers: displaying the hypotheses and current goals as an argument is being developed, as well as using automated reasoning to fill in gaps that have been implied (Tran Minh, Gonnord and Narboux, 2025), which should help support students in tracking the progress of their argumentation.
Additionally, since we intend to use GenAI, we can use it to provide students with feedback based on the verification of their arguments. To mitigate concerns that usage could encourage over-dependence on GenAI, diminish critical thinking, and reduce skills retention (Bittle and El-Gayar, 2025, Digital Education Council, 2026), we should design the AI Agent to function as a learning companion with students remaining responsible for the reasoning process (Coursera, 2026).
In collaborative argumentation, an iterative process of adding comments contributes towards reaching a solution, even if the formal verifications are incorrect as they can then be excluded (Almpani, Stefaneas and Vandoulakis, 2023).
To ensure this process supports students’ argumentation skills development, the tool should encourage self-explanation practices by allowing students to be immersed into a process of verifying one step at a time, identifying the main ideas being applied, and explaining how they connect to earlier steps or facts (Balan, 2025):
- The first step can be enforced by constraining GenAI’s outputs to one formal statement per reasoning step, which should improve the accuracy of outputs.
- The second step should result naturally as, since AI can misinterpret students’ reasoning (Kaldaras and Haudek, 2022), students will be required to critically evaluate failures in argument verification, which should also reduce skill atrophy and AI complacency (Z. Lin and Sohail, 2026).
- By revising and explaining their reasoning in more detail, students take on a “learning-by-teaching” approach which completes the self-explanation loop. This interaction can enhance metacognitive skills (Gao, 2026) and could be used by a teacher to determine whether additional direct instruction is required (Song and Sparks, 2019a).
Additionally, as we need to explicitly teach students how to self-explain (Balan, 2025), we require clear onboarding to introduce and justify the intended game experience.
As we want to ensure the AI Agent to enhance learning instead of replacing any teaching and reasoning, we should design the AI Agent to guide the student by constraining responses to questions and response templates, prompting the student to refine and extend their thinking (Gao, 2026). This allows us to safely build in basic directions anticipated by a teacher by defining solution snippets/hints and conditions which, once met, are provided to the AI Agent so responses can be phrased to gently guide the student towards the correct solution path. This intervention offers an alternative route into engagement where students can rehearse and explore reasoning in a more interactive, adjustable and explanation-focused environment (Gao, 2026, Jamaludin,Ho and Chee, 2007, W.-C. Lee and Lai, 2024).
Lastly, taking into account emotional needs:
- Argumentation verification should support learning by minimising consequences for failures to encourage risk-taking and deeper exploration (Tatnall, 2020).
- In anticipation of students choosing to personalise their experience with the inclusion of stressful stimuli, it is a requirement that we provide the opportunity to pause, debrief and structured self-reflection in order to mitigate the negative impacts of stress on learning (Falon et al., 2022, Y. Liu et al., 2025, Mekler, Iacovides and Bopp, 2018).
3.1 Summary
Overall, this verification loop meets the description of “authentic demonstration of learning” provided by Robert et al. (2026) as emphasising “process, reasoning, explanation, collaboration, oral explanation, and critical evaluation of AI interpretation”. Though the collaboration is with an AI Agent in this context, we have included social play in our plan for potential future development in the appendix.
We also avoid three assumptions: - that games are inherently engaging; - that AI is inherently harmful; - or, that accessibility can be acknowledged retroactively.
This links to the challenge, outcomes and technology choice by treating the game as a restricted formative alternative for argumentation practice, instead of replacing teaching, assessment or academic support.
However, as this is more complex than a simple argument-mapping activity, it also comes with higher risk. Therefore, a responsible first step would be to focus on a few argumentation scenarios and test whether students understand and benefit from the automated assessment-feedback loop before scaling (Pei, Du and Jin, 2025, Tran Minh, Gonnord and Narboux, 2025).
4 Project Plan
4.1 Solution Overview
Using the Mechanics-Dynamic-Aesthetics framework (Hunicke, LeBlanc and Zubek, 2004), we can summarise our solution as:
- The student and Small Language Model (SLM) will collaboratively roleplay as a single protagonist’s chain of thought using natural language, aiming to arrive at a solution for a given scenario. The intended experience is low-stakes challenge with optional performance pressure.
- The student explains their reasoning, the SLM responds with a template responses or Socratic questioning, and the student revises their reasoning in response. This repeats until a solution is reached.
- Using the SLM and an intermediary graph representation as translation layers, the student interacts with formal verification systems by expressing their reasoning. The intermediary graph representation assists the SLM in natural language processing as well as enabling optimisation and algorithms to determine fact dependencies and appropriate student hints.
The project will use the Plan, Do, Check, Act/Review cycle with the following project milestones:
- Develop an intermediary graph representation, building in mapping accuracy and scaffolded responses.
- Refine the assessment-feedback loop for a selection of scenarios.
- Build an accessible user interface for gameplay, reviewed with student testing on a selection of scenarios.
- Build an accessible user interface for customising/importing scenarios, reviewed with student testing.
Throughout, we would need to ensure we design and prepare for institutional review (The University of Manchester, no date), accessibility testing (CAST, 2024, W3C Accessibility Guidelines Working Group, 2024), human validation (Kaldaras and Haudek, 2022, L. Kong and Shin, 2026) and a supported data protection model (The University of Manchester, 2026b).
4.2 Student Interaction Storyboard
To storyboard the active assessment-feedback loop, we shall use the “Riddle of Two Guards” problem as our example scenario and Isabelle/HOL as our example formal verification system:
There are two doors, each with a guard stood in front, one is a truth-teller, the other is a liar, and only one of the doors leads to safety. You are allowed to ask one guard a single yes-or-no question.
Example of verified step:
- Student: “If I ask ‘Is this door safe?’, the TruthTeller will state that the door is safe if it actually is safe.”
- SLM processes this into an intermediary graph representation that identifies claim dependencies.
- The intermediary graph representation outputs Isabelle/HOL code for verification, including:
```{isabelle}
lemma truth_teller_reports_safety:
assumes "guard_at w g = TruthTeller"
assumes "door_is_safe w d"
shows "answers (guard_at w g) (door_is_safe w d)"
using assms
unfolding door_is_safe_def
by simp
```- Isabelle/HOL verifies this alongside previously verified facts.
- The intermediary graph representation communicates this verification.
- Example Response: “Yeah that checks out…”
- The student builds on this by providing their next step in reasoning.
| Step | Description | If the student skips straight to the solution | If the student makes an incorrect argument |
|---|---|---|---|
| 4 | Isabelle/HOL verification | Fails as the reasoning to conclude the solution is absent | Fails |
| 5 | Intermediary Graph | Communicates failure | Communicates failure with any relevant hints |
| 6 | Example Response/s | “How do I know for sure that that would work?” | “Let’s break that down into smaller steps.” |
| “But why would that work?” | |||
| “Have I considered all possible cases?” | |||
| “But that feels incorrect because …” | |||
| “What about/if … ?” |
Thus, this activity directly supports the short-term outcomes by requiring students to synthesise reasoning, revise it through conversation, and apply argumentation principles within a scenario. The appendix includes a full example of the Isabelle/HOL code for this scenario.
5 References
6 Appendix Items
6.1 Isabelle/HOL Full Example Code
This appendix demonstrates that the proposed verification approach is technically feasible and that natural-language reasoning can be translated into formally verifiable statements.
The following code was iteratively developed with Copilot so that I could translate my ideas into a verifiable example, which also indicates GenAI as a potential assistant within a scenario customisation interface.
```{isabelle}
theory Riddle_of_Two_Guards
imports Main
begin
(* There are two doors, each with a guard stood in front,
one is a truth-teller, the other is a liar,
and only one of the doors leads to safety. *)
datatype position =
Left
| Right
fun other_position :: "position ⇒ position" where
"other_position Left = Right"
| "other_position Right = Left"
datatype guard =
TruthTeller
| Liar
fun other_guard :: "guard ⇒ guard" where
"other_guard TruthTeller = Liar"
| "other_guard Liar = TruthTeller"
datatype door =
Safe
| Unsafe
definition other_door :: "position ⇒ position" where
"other_door = other_position"
record world =
door_at :: "position ⇒ door"
guard_at :: "position ⇒ guard"
definition valid_world :: "world ⇒ bool" where
"valid_world w ⟷
door_at w Left ≠ door_at w Right
∧ guard_at w Left ≠ guard_at w Right"
definition door_is_safe :: "world ⇒ position ⇒ bool" where
"door_is_safe w p ⟷ door_at w p = Safe"
(* You are allowed to ask one guard a single yes-or-no question. *)
(* A truth-teller answers honestly.
A liar will always answer the opposite. *)
fun answers :: "guard ⇒ bool ⇒ bool" where
"answers TruthTeller p = p"
| "answers Liar p = (¬ p)"
(* -- Draft Attempt -- *)
(* If I ask "Is this door safe?" the TruthTeller will state that
the door is safe when it really is safe. *)
lemma truth_teller_reports_safety:
assumes "guard_at w g = TruthTeller"
assumes "door_is_safe w d"
shows "answers (guard_at w g) (door_is_safe w d)"
using assms
unfolding door_is_safe_def
by simp
(* If I ask "Is this door safe?" the other guard would have said the opposite. *)
lemma other_guard_answers_opposite:
"answers (other_guard (guard_at w g))
(door_is_safe w d)
=
(¬ answers (guard_at w g)
(door_is_safe w d))"
by (cases "guard_at w g") simp_all
(* If I ask "Would the other guard say this door is safe?" *)
definition other_guard_answer ::
"world ⇒ position ⇒ position ⇒ bool"
where
"other_guard_answer w g d =
answers
(guard_at w g)
(answers
(other_guard (guard_at w g))
(door_is_safe w d))"
(* If I ask the TruthTeller what the other guard would say,
the TruthTeller reports the lie. *)
lemma other_guard_answer_truth_teller:
assumes "guard_at w g = TruthTeller"
shows "other_guard_answer w g d =
(¬ door_is_safe w d)"
using assms
unfolding other_guard_answer_def
by simp
(* If I ask the Liar what the other guard would say,
the Liar lies about the TruthTeller's answer,
producing the same lie. *)
lemma other_guard_answer_liar:
assumes "guard_at w g = Liar"
shows "other_guard_answer w g d =
(¬ door_is_safe w d)"
using assms
unfolding other_guard_answer_def
by simp
(* Regardless of which guard is asked,
the answer is the opposite of the truth. *)
theorem two_guards_solution:
"other_guard_answer w g d =
(¬ door_is_safe w d)"
unfolding other_guard_answer_def
by (cases "guard_at w g") simp_all
(* Therefore a "no" answer means the tested door is safe. *)
theorem choose_tested_door_when_answer_is_no:
"(other_guard_answer w g d = False)
⟷ door_is_safe w d"
using two_guards_solution
by simp
end
```6.2 Implementation Feasibility & Responsible AI Use
The full feasibility argument is that this is a technically ambitious, mission-led educational game rather than a simple content resource. Development literature warns that non-profit or educational game projects require labour, technical judgement, inclusion work, documentation, testing and resourcing (Freeman et al., 2023, King, 2026).
However, Madanamootoo and Alla (2026) argues that GenAI is becoming a democratising force in game production for independent developers within the US, evidenced by:
- Replacing 1-2 weeks of producer time spent on creating a completely structured production plan to around 5 minutes using GenAI;
- Reducing $2,400-4,800 overhead cost on production plans with $0.27-0.58 of GenAI cost with less dependence on production-management training;
- Significant year-by-year increases in indie game releases between 2024-2026;
- AI-disclosed releases had a median positive-review ratio of 85.9% compared to 97.8% for non-disclosed releases;
- AI-disclosed releases are commercially accepted at scale.
Unfortunately, they were not able to conclude whether AI-disclosed releases received worse reception than non-disclosed titles nor whether the judgement quality of AI-generated plans were comparable to human producers. Given there doesn’t appear to be any enforceable standards of AI practice in the game development industry beyond being required to disclose AI use, we can default to following the University of Manchester’s AI Guidelines (The University of Manchester, 2026a).
The recent release of GPT 6 Astra also demonstrates promising results in coding and game development (OpenAI, 2026). Though actual performance would need to be verified within the context of our project and it is relatively expensive compared to other models, it could prove invaluable as an assistive tool in large-scale coding tasks.
Fortunately, we have minimised the project plan for the game development by moving “nice to have” features into plans for potential future development. I have also managed to use tutorials to develop an AI chat interface in Godot Engine, an open-source game engine. Thus, the main technical challenges of the work required include:
- Defining the intermediary representation and deterministic maps to Prolog and Isabelle/HOL.
- Integrating Google’s LiteRT framework to allow the small LLMs designed for edge devices to be packaged as part of the game as well as run efficiently.
- Packaging Prolog and Isabelle/HOL so they can run within the exported game executable.
The third challenge is anticipated to be the most difficult due to their complex architectures dependent on multiple programming languages and it is unknown whether it would be easier to instead develop a hybrid system from scratch or find a way to get Isabelle/HOL to be run directly in browser using WebAssembly (WASM). If we cannot meet the third step, that would limit the game from running on mobile devices.
6.3 Plan for Potential Future Development
These are possible features we can implement after project success:
- Optimise the backend system so the sandbox can be hosted on a wider range of devices.
- Develop a more advanced user interface that allows students to switch to visualised representations of argumentation.
- Design a Quarto extension that allows Staff to generate scenarios as a consequence of preparing accessible teaching resources.
- Develop the option for multiplayer to enable social play and peer-based learning and integrate with third-party services to enable students to easily share their argumentation scenarios with the wider community.
6.3.1 Optimised Backend
A future hybrid Prolog and Isabelle/HOL architecture may be preferable because the two tools support different reasoning strengths but the use of both systems in parallel will lead to some verifications being repeated in both systems. Isabelle/HOL is appropriate for higher-assurance proof-style verification, while Prolog could represent relational, rule-based and more holistic reasoning patterns that are not always natural to express as bottom-up proof obligations.
This matters because analytic and holistic thinking styles may emphasise different relationships, contexts and dependencies. The intermediary graph should therefore avoid assuming one reasoning style: it should preserve enough structure to map into Isabelle/HOL for proof-style checks and into Prolog for relational verification. More research and evaluation is required to determine whether combining Prolog and Isabelle/HOL would actually result in a more interculturally inclusive tool.
6.3.2 Visualised Representations
The current proposal uses the graph internally to connect natural-language reasoning to Isabelle/HOL verification. A later version could make that graph visible and editable, allowing students either to reason through language with the AI agent or to contribute directly to the graph by adding claims, warrants, objections, definitions or dependencies. Building the intermediary graph representation by starting with the Argument Interchange Format (Argumentation Research Group, University of Dundee, 2011) would help ensure the visualised interaction is intuitive.
This would support Universal Design for Learning because it provides another route for action and expression (CAST, 2024) in developing argumentation skills while preserving the core verification loop. Some students may prefer to explain reasoning in prose; others may find it easier to manipulate visible relationships between claims. Argument-visualisation literature supports this possibility because visualising claims, warrants, objections and dependencies can reduce working-memory load and make reasoning inspectable, provided students receive sufficient instruction and guided practice (D. Chang, M. P.-C. Lin and Hwang, 2025, Davies and Calma, 2026, M. P.-C. Lin et al., 2026, Nesbit and Q. Liu, 2025).
The future feature should therefore be designed as an optional graph-view and graph-edit mode, not as a required replacement for roleplayed dialogue. It would need separate onboarding, examples, accessibility checks and validation because complex mapping features can also be a source of extraneous cognitive load for novices.
This is something I had already started developing in Godot Engine, until I realised I needed to define the intermediary representation first and that I might have been getting ahead of myself.
6.3.3 Integration with Existing Tools & Developments
On top of digital solutions minimising staff burden by catering to students as an assistive tool, it should remain compatible with existing customisable multi-format resource rendering workflows, including Quarto (quarto-dev, 2026c, 2026b, 2026a).
This could be done by building an extension that embeds knowledge graph extraction into the Quarto rendering process design to output a formally verified graph that meets our intermediary representation schema. The current cost and effectiveness of this is unknown but GenAI is continuing to advance at a rapid pace.
I decided our current project shouldn’t explore this as active developments in Generative Educational Resources (Coursera, 2026, LearnLM Team, 2025) and WAI-Adapt (Atkinson, Sajka and Wolberger, 2026) should eventually lead to guidance that informs this solution.
6.3.4 Social Play
Inquiry, collaborative argumentation and roleplay literature supports prompts for claims, evidence, counterarguments, perspective comparison and probing questions, while warning that risk to reputation can reduce participation (Ibrahim and Harun, 2015, Jamaludin,Ho and Chee, 2007, Jha, Bhowmik and Bhagat, 2024). This evidence remains useful for future iterations that introduce peer comparison or social play, but the assessed prototype keeps the first interaction private and AI-mediated.
Buzzfeed’s Cultural Cartography (Nguyen, 2018) and Garry’s Mod, a physics-based sandbox, (Facepunch Studios, 2026) work as inspirations that motivate the desire to make sharing customised scenarios as easy as possible in order to increase engagement and target viral marketing. I also feel there is a gap in the market around high-intensity emergent gameplay dependent on argumentation and problem-solving, particularly when it comes to transferring fictional worlds based on academic/scientific environments into video game format. Filling this gap requires a formal verification backend to be developed that avoids restricting player options to a finite set of approaches and makes the most out of their creativity.