© 1988 by British Computer Society
| ||||||||||||||||||||||||||||||||||||||||||||||||||
VDM: Axiomatising its Propositional Logic
Faculty of Mathematics, The Open University, Milton Keynes MK7 6AA, UK
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.
Received April 1987. revised May 1987.
* Faculty of Mathematics, The Open University, Milton Keynes MK7 6AA, England