 The BIO interface mostly takes the form of Prover-Skeptic games inspired from Sørensen and Urzyczyn (2006), which developed a dialogical framework motivated by questions in the study of computation. In the BIO, the Prover (or proponent) is the player who proves that the conclusion of the deduction follows from the premises, and the Skeptic (or opponent) is the player who doubts each step of the proof and who will raise objections if he can. The game starts with Prover asking Skeptic to grant the premises, which Skeptic accepts for the sake of the argument. Then Prover states what necessarily follows from these premises, and Skeptic’s role is to make sure that each new statement made by Prover clearly follows from the previous statements. Prover can thus provide counter-examples to a statement or ask clarifications (“why does this follow?”). Skeptic’s role is thus to check that the proof is compelling. The play is asymmetric, since Prover defends and Skeptic attacks.