As a Professor, I want to ask proof questions, so that I can assess my student's logic process

[pandasa123]

Background

Professors test students with proof questions. This typically involve:

Given X Show Y

Where X and Y are usually pseudo-code...probably closer to LaTeX. Here's an example for Turing Decidability in classical computing theory (where decidable is a language that either accepts or halts without loops):

State if the following language is decidable or undecidable

$L_{HALT \geq 10} = \{ (\langle M \rangle, x) \}$: M halts on x after running for at least 10 steps

Where the proof is as follows:

This language is undecidable. We can show this with a reduction from the Halting Problem with a language as follows:

Given a blackbox decider $B{HALT \geq 10}$ for $L{HALT \geq 10}$, we construct the following for decider $H{HALT}$ for $L{HALT}$

1. Construct the Machine $M' =$ 'On input $\omega:$ A. Run for 10 steps with no actions B. Run M on $\omega$ and output the same answer (if M ever halts)'
2. Call blackbox decider $B_{HALT \geq 10} (\langle M' \rangle, x) $ and output the same answer

Analysis:

1. $H_{HALT}$ halts on every input so it is a valid decider
2. $H{HALT} (\langle M \rangle, x)$ accepts if and only if $M(x)$ halts: a. $M$ halts on $x$ $\implies M'$ halts on $x$ after at least 10 steps $\implies B{HALT \geq 10} (\langle M' \rangle, x)$ accepts $\implies H{HALT} (\langle M \rangle, x)$ accepts b. $M$ loops on $x$ $\implies M'$ loops on $x$ $\implies B{HALT \geq 10} (\langle M' \rangle, x)$ $\implies H_{HALT} (\langle M \rangle, x)$ rejects

Therefore, $H$ is a decider for $L{HALT}$. This shows that $L{HALT}$ is a reduction of $L{HALT \geq 10}$. Since $L{HALT}$ is undecidable, so is $L_{HALT \geq 10}$

Goal

We should be able to support auto-grading these problems for Professors

Possible idea:

Client side example of using drop down example and push to server side grading over time?

Acceptance criteria

• [ ] Work with design team to create an interactive design for one proof problem
• [ ] Validate with 3+ professors
• [ ] Investigate auto-grading

Out of scope

Full implementation with server isn't needed yet, same with professor definition. We just need to show one provocative example, could be a design to test

Resources

No response

Tasks

No response

[pandasa123]

Proofs are a bit wider and more generalised...maybe we can look towards "given two states, design a procedure to connect" in code instead?

[vabarbosa]

This repository is no longer maintained. It has been superseded by IBM Quantum Learning.