Formalization of proofs using relational calculus

Yoshihiro Mizoguchi, Hisaharu Tanaka, Shuichi Inokuchi

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Abstract

    We introduce a theory of relations and a method to prove using relational calculus. Several notions in mathematics and computer science are formalized using relational expressions. Propositions described by relational expressions can be solved by relational calculus, symbolic computations. We propose to apply our formalization to proofs in coding theory especially formalizations of algorithms including an error-correcting algorithm using automata. We introduce a formalization of notions in category theory and automata theory using relational expressions. We also show a formalization of an elementary theory of relations in Coq, a proof assistant system. We introduce an automatic proving procedures (tactics) for our formalization of the theory of relational calculus.

    Original languageEnglish
    Title of host publicationProceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016
    PublisherInstitute of Electrical and Electronics Engineers Inc.
    Pages527-531
    Number of pages5
    ISBN (Electronic)9784885523090
    Publication statusPublished - Feb 2 2017
    Event3rd International Symposium on Information Theory and Its Applications, ISITA 2016 - Monterey, United States
    Duration: Oct 30 2016Nov 2 2016

    Publication series

    NameProceedings of 2016 International Symposium on Information Theory and Its Applications, ISITA 2016

    Other

    Other3rd International Symposium on Information Theory and Its Applications, ISITA 2016
    Country/TerritoryUnited States
    CityMonterey
    Period10/30/1611/2/16

    All Science Journal Classification (ASJC) codes

    • Computer Networks and Communications
    • Hardware and Architecture
    • Information Systems
    • Signal Processing
    • Library and Information Sciences

    Fingerprint

    Dive into the research topics of 'Formalization of proofs using relational calculus'. Together they form a unique fingerprint.

    Cite this