• Login
    View Item 
    •   Repository Home
    • Brock Theses
    • Masters Theses
    • M.Sc. Computer Science
    • View Item
    •   Repository Home
    • Brock Theses
    • Masters Theses
    • M.Sc. Computer Science
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    L-Fuzzy Relations in Coq

    Thumbnail
    View/Open
    Ethan Jackson - MSc Thesis (469.5Kb)
    Date
    2014-09-05
    Author
    Jackson, Ethan
    Metadata
    Show full item record
    Abstract
    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.
    URI
    http://hdl.handle.net/10464/5673
    Collections
    • M.Sc. Computer Science

    Brock University | Copyright © 2006-2015 
    Contact Us | Send Feedback
     

     

    Browse

    All of DSpaceCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    LoginRegister

    Statistics

    View Usage Statistics

    Brock University | Copyright © 2006-2015 
    Contact Us | Send Feedback