Abstract: This gives a brief introduction to the interactive proof editor (Ritchie, Cartmell and Hagino) which enables one to create proofs in first order logic with induction. It is implemented using attribute grammar evaluation. It also describes briefly work by Plotkin, Harper and Honsell on the ``logical framework'', a general proof editor for arbitrary natural deduction logics.
Previous | Index | Next An error occured whilst processing this directive