Research in Interactive Theorem Proving at Edinburgh University

R.M. Burstall

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.

LFCS report ECS-LFCS-86-12

Previous | Index | Next