A certified reduction strategy for homological image processing

  1. Poza, M. 1
  2. Dominguez, C. 1
  3. Heras, J. 2
  4. Rubio, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

  2. 2 University of Dundee
    info

    University of Dundee

    Dundee, Reino Unido

    ROR https://ror.org/03h2bxq36

Zeitschrift:
ACM Transactions on Computational Logic

ISSN: 1529-3785

Datum der Publikation: 2014

Ausgabe: 15

Nummer: 3

Seiten: 23

Art: Artikel

DOI: 10.1145/2630789 SCOPUS: 2-s2.0-84907581196 WoS: WOS:000343693300006 arXiv: 1306.0806 GOOGLE SCHOLAR lock_openOpen Access editor

Andere Publikationen in: ACM Transactions on Computational Logic

Zusammenfassung

The analysis of digital images using homological procedures is an outstanding topic in the area of Computational Algebraic Topology. In this paper, we describe a certified reduction strategy to deal with digital images, but preserving their homological properties. We stress both the advantages of our approach (mainly, the formalisation of the mathematics allowing us to verify the correctness of algorithms) and some limitations (related to the performance of the running systems inside proof assistants). The drawbacks are overcome using techniques that provide an integration of computation and deduction. Our driving application is a problem in bioinformatics, where the accuracy and reliability of computations are specially requested