A typed logic of partial functions reconstructed classically
type: Item
instance of: scholarly article
title: A typed logic of partial functions reconstructed classically
zbMATH Open document ID: 0804.03018
DOI: 10.1007/BF01178666
author: V. Pereyra
published in: Acta Informatica
publication date: 1995-01-24T00:00:00Z
review text: This paper gives a comprehensive description of a typed version of the logic known as LPF. This logic is basic to formal specification and verified design in the software development method VDM. If appropriately extended to deal with recursively defined functions, the data types used in VDM, etc., it gives the VDM notation and its associated rules of reasoning. The paper provides an overview of the needed extensions and examines some of them in detail. It is shown how this nonclassical logic -- and the extensions -- can be reconstructed classically by embeddings into classical infinitary logic.
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 695001
zbMATH Keywords: logic LPF
zbMATH Keywords: formal specification
zbMATH Keywords: verified design
zbMATH Keywords: software development method VDM
zbMATH Keywords: embeddings into classical infinitary logic
MaRDI profile type: Publication
cites work: A logic covering undefinedness in program proofs
cites work: Q4296956
cites work: Model theory for infinitary logic. Logic with countable conjunctions and finite quantifiers
full work available at URL: https://doi.org/10.1007/bf01178666
OpenAlex ID: W2030221869
description: scientific article; zbMATH DE number 695001