Septe Mb Er, Bernard Sufrin, Richard Bornat
In this note we show how Jape's presentations of proofs are related to the natural-deduction presentations used by Jim Woodcock and Jim Davies in [7] ("the book"). This is followed by...
Using J'n'J in Unix/X JAPE: Natural Deduction using the Jape Proof Editor (2007)
Bernard Sufrin, Richard Bornat
In this note we describe, by means of a number of case studies, the user interface to the Jape implementation -- "J'n'J" -- of the logic described in [7] ("the book")....
1 Getting Started with J'n'J (2007)
Bernard Sufrin, Richard Bornat
In this note we describe, by means of a number of case studies, the user interface to the Jape implementation { \J'n'J " { of the logic described in [7] (\the book"). The...
Animating Operational Semantics with Jape (2007)
Bernard Sufrin, Richard Bornat
In this note we give a brief introduction to the ideas of operational semantics and show how to use Jape to animate the operational semantics of a couple of simple programming languages. We give the...
J'n'J in Jape Encoding a Natural Deduction System for the Jape Proof Editor (2007)
Bernard Sufrin, Richard Bornat
In this note we show how Jape's presentations of proofs are related to the naturaldeduction presentations used by Jim Woodcock and Jim Davies in [7] (\the book"). This is followed by...
A content-addressable file store / (2004)
Mueller, Phil C., Sufrin, Bernard.
Supervisor : Bernard Sufrin.
A content-addressable file store / (2004)
Mueller, Phil C., Sufrin, Bernard.
Supervisor : Bernard Sufrin.
Aczel, James, Fung, Pat, Bornat, Richard, Oliver, Martin, O'Shea, Tim, Sufrin, Bernard
This paper describes a research project into undergraduates’ use of a software tool to learn symbolic logic—a complex abstract domain that has been shown to be intimidating for students. The...
Using computers to learn logic: undergraduates' experiences (1999)
Aczel, James, Fung, P., Bornat, Richard, Oliver, Martin, O'Shea, Tim, Sufrin, Bernard
Learning formal logic can be difficult for many students. This paper describes some ongoing research into a computer program designed to help computer science undergraduates learn the natural...
Using computers to learn logic: undergraduates' experiences (1999)
Aczel, James, Fung, P., Bornat, Richard, Oliver, Martin, O'Shea, Tim, Sufrin, Bernard
Learning formal logic can be difficult for many students. This paper describes some ongoing research into a computer program designed to help computer science undergraduates learn the natural...
Modeless Structure Editing (1999)
this paper we honour Tony by building a simple model of structure editing to serve as a basis for the design of a family of editors. Structure editors make it easy to perform edit actions in which...
User Interfaces for Generic Proof Assistants Part I: Interpreting Gestures (1998)
Bernard Sufrin, Richard Bornat
JAPE is a generic proof editor which (amongst other things) offers the teacher, user, or logic designer the opportunity of constructing a direct manipulation interface for proofs. In part I of this...
Richard Bornat, Bernard Sufrin
Jape is a proof editor designed for use by novices and to be programmed by tyro logicians. Its user interface intrudes as little as possible into the business of making and writing down a proof; its...
Formalisation of aspects of office automation / (1983)
Urundolil-Kumaran, Jeevan., Sufrin, Bernard.
Supervisor : Steve Schuman.
Richard Bornat, Bernard Sufrin
IONAA) IS FROMX=YANDAA(Y) INFER AA(X) 1 The ABSTRACTION annotation directs Jape to interpret the juxtaposition formulæ AA(Y) and AA(X) as shorthand for substitution forms. The parameter X allows us...