Show simple item record

dc.contributor.authorJackson, Ethan
dc.date.accessioned2014-09-05T15:12:07Z
dc.date.available2014-09-05T15:12:07Z
dc.date.issued2014-09-05
dc.identifier.urihttp://hdl.handle.net/10464/5673
dc.description.abstractHeyting categories, a variant of Dedekind categories, and Arrow categories provide a convenient framework for expressing and reasoning about fuzzy relations and programs based on those methods. In this thesis we present an implementation of Heyting and arrow categories suitable for reasoning and program execution using Coq, an interactive theorem prover based on Higher-Order Logic (HOL) with dependent types. This implementation can be used to specify and develop correct software based on L-fuzzy relations such as fuzzy controllers. We give an overview of lattices, L-fuzzy relations, category theory and dependent type theory before describing our implementation. In addition, we provide examples of program executions based on our framework.en_US
dc.language.isoengen_US
dc.publisherBrock Universityen_US
dc.subjectL-Fuzzy Relationsen_US
dc.subjectAllegoriesen_US
dc.subjectArrow Categoriesen_US
dc.subjectCoqen_US
dc.titleL-Fuzzy Relations in Coqen_US
dc.typeElectronic Thesis or Dissertationen
dc.degree.nameM.Sc. Computer Scienceen_US
dc.degree.levelMastersen_US
dc.contributor.departmentDepartment of Computer Scienceen_US
dc.degree.disciplineFaculty of Mathematics and Scienceen_US
dc.embargo.termsNoneen_US
refterms.dateFOA2021-07-31T01:37:09Z


Files in this item

Thumbnail
Name:
Brock_Jackson_Ethan_2014.pdf
Size:
469.5Kb
Format:
PDF
Description:
Ethan Jackson - MSc Thesis

This item appears in the following Collection(s)

Show simple item record