Formally Verified Conditions for Regularity of Interval Matrices

Ioana Pasca 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We propose a formal study of interval analysis that concentrates on theoretical aspects rather than on computational ones. In particular we are interested in conditions for regularity of interval matrices. An interval matrix is called regular if all scalar matrices included in the interval matrix have non-null determinant and it is called singular otherwise. Regularity plays a central role in solving systems of linear interval equations. Several tests for regularity are available and widely used, but sometimes rely on rather involved results, hence the interest in formally verifying such conditions of regularity. In this paper we set the basis for this work: we define intervals, interval matrices and operations on them in the proof assistant Coq, and verify criteria for regularity and singularity of interval matrices.
Type de document :
Communication dans un congrès
Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, 6167, pp.219-233, 2010, LNAI
Liste complète des métadonnées

Littérature citée [1 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00464937
Contributeur : Ioana Pasca <>
Soumis le : jeudi 18 mars 2010 - 14:31:38
Dernière modification le : jeudi 11 janvier 2018 - 16:23:44
Document(s) archivé(s) le : vendredi 19 octobre 2012 - 10:10:26

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00464937, version 1

Collections

Citation

Ioana Pasca. Formally Verified Conditions for Regularity of Interval Matrices. Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Calculemus, Jul 2010, Paris, France. Springer, 6167, pp.219-233, 2010, LNAI. 〈inria-00464937〉

Partager

Métriques

Consultations de la notice

373

Téléchargements de fichiers

176