logics Notes Create a language that allows the user to construct proofs (i.e sequences of transformations from a given input to output) How should the proof/program be formatted? Generate LaTeX? How should the rules be formatted? Generate LaTeX? How can an inductive proof be given? base case / inductive step / ??? Can the computation of proofs be optimised? e.g. by combining several steps int one transformation Can parts of the proof be reformatted as theorems/lemmas?
