In Vulcan’s Project Halo, we developed means of extracting the structure of logical proofs that answer advanced placement (AP) questions in biology. For example, the following shows a proof that separation of chromatids occurs during prophase.
This explanation was generated using capabilities of SILK built on those described in A SILK Graphical UI for Defeasible Reasoning, with a Biology Causal Process Example. That paper gives more details on how the proof structures of questions answered in Project Sherlock are available for enhancing the suggested questions of Inquire (which is described in this post, which includes further references). SILK justifications are produced using a number of higher-order axioms expressed using Flora‘s higher-order logic syntax, HiLog. These meta rules determine which logical axioms can or do result in a literal. (A literal is an positive or negative atomic formula, such as a fact, which can be true, false, or unknown. Something is unknown if it is not proven as true or false. For more details, you can read about the well-founded semantics, which is supported by XSB. Flora is implemented in XSB.)
Now how does all this relate to pedagogy in future derivatives of electronic learning software or textbooks, such as Inquire?
Well, here’s a use case: Continue reading “Pedagogical applications of proofs of answers to questions”