This paper compares the finitary three-valued logic LPF and the infinitary two-valued logic MPLω, the logics underlying VDM SL and COLD-K. These logics reflect different approaches to reasoning about partial functions and bringing recursive function definitions into proofs. The purpose of the comparison is to acquire insight into the relationship between these approaches. A natural translation from LPF to MPLω is given. It is shown that what can be proved remains the same after translation, in case strictness axioms are added to LPF or removed from MPLω. The translation from LPF to MPLω is extended to recursive function definitions and this translation is next used to justify some ways of bringing the definitions of partial functions into proofs using LPF.
CITATION STYLE
Middelburg, C. A., & Renardel De Lavalette, G. R. (1991). LPF and MPLω — A logical comparison of VDM SL and COLD-K. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 551 LNCS, pp. 279–308). Springer Verlag. https://doi.org/10.1007/3-540-54834-3_18
Mendeley helps you to discover research relevant for your work.