White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Unifying Theories of Logics with Undefinedness

Bandur, Victor (2014) Unifying Theories of Logics with Undefinedness. PhD thesis, University of York.

[img]
Preview
Text (Doctoral thesis)
Report.pdf - Examined Thesis (PDF)
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (1707Kb) | Preview

Abstract

A relational approach to the question of how different logics relate formally is described. We consider three three-valued logics, as well as classical and semi-classical logic. A fundamental representation of three-valued predicates is developed in the Unifying Theories of Programming (UTP) framework of Hoare and He. On this foundation, the five logics are encoded semantically as UTP theories. Several fundamental relationships are revealed using theory linking mechanisms, which corroborate results found in the literature, and which have direct applicability to the sound mixing of logics in order to prove facts. The initial development of the fundamental three-valued predicate model, on which the theories are based, is then applied to the novel systems-of-systems specification language CML, in order to reveal proof obligations which bridge a gap that exists between the semantics of CML and the existing semantics of one of its sub-languages, VDM. Finally, a detailed account is given of an envisioned model theory for our proposed structuring, which aims to lift the sentences of the five logics encoded to the second order, allowing them to range over elements of existing UTP theories of computation, such as designs and CSP processes. We explain how this would form a complete treatment of logic interplay that is expressed entirely inside UTP.

Item Type: Thesis (PhD)
Academic Units: The University of York > Computer Science (York)
Depositing User: Mr Victor Bandur
Date Deposited: 29 Nov 2016 12:15
Last Modified: 29 Nov 2016 12:15
URI: http://etheses.whiterose.ac.uk/id/eprint/15405

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)