L-Fuzzy Relations in Coq

Heyting 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.

Name thesis:degree_name

M.Sc. Computer Science

Level thesis:degree_level

Masters

Discipline thesis:degree_discipline

Faculty of Mathematics and Science

Department dc:contributor.department

Department of Computer Science

Grantor

Brock University

Year dc:date.issued

2014

Author dc:creator

• Jackson, Ethan

• L-Fuzzy Relations
• Allegories
• Arrow Categories
• Coq

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/10464/5673

OAI identifier oai:identifier

oai:brocku.scholaris.ca:10464/5673