next up previous contents
Next: Rule applications Up: Proof semantics Previous: Proof semantics   Contents

The assumption base

NDL maintains a global set of formulas called the assumption base. We can think of the elements of the assumption base as our premises--formulas that we regard as true. Initially the system starts with the empty assumption base. Every time an assertion is made or a theorem is proved, the corresponding formula is inserted into the assumption base. We will use the letter $\beta$ to designate a typical assumption base. In what follows we describe the semantics of each possible type of NDL proof. A key idea behind NDL is that the meaning of a proof is a function over assumption bases. Put more plainly, the meaning of a proof depends on what assumption base we evaluate that proof in. This is similar to how the meaning of an imperative program is formally captured. We say that the meaning of x := y + 3; is a function over stores. That is, the result we get by executing this instruction depends on (or ``is relative to'') a given store. Note: the assumption base can be inspected at any point by selecting Options and then View assumption base from the top menu bar.
next up previous contents
Next: Rule applications Up: Proof semantics Previous: Proof semantics   Contents
2004-08-04