VDM: Axiomatising its Propositional Logic
Peter Gibbins · The Computer Journal · 1988
The 3-valued truth-tables of LPF, which is both the logic of partial functions and also the logic of VDM, do not determine the logic unless the appropriate notion of logical consequence is specified. Three alternative notions of logical consequence are considered and LPF is axiomatised as a sequent calculus for each such notion. The three axiomatisations employ the same introduction rules for the connectives and differ only in their axiom sequents. The axiomatisations lead naturally to automatic theorem-provers for LPF.