Bandur, Victor (2014) Unifying Theories of Logics with Undefinedness. PhD thesis, University of York.
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.
Metadata
Supervisors: | Woodcock, Jim |
---|---|
Awarding institution: | University of York |
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 |
Open Archives Initiative ID (OAI ID): | oai:etheses.whiterose.ac.uk:15405 |
Download
Examined Thesis (PDF)
Filename: Report.pdf
Description: Doctoral thesis
Licence:
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 2.5 License
Export
Statistics
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.