CHEYNET-SOUBOU, M Sadry (2020) Extension de la méthode des tableaux aux intervalles de flottants PRE - Research Project, ENSTA.



In the context of hybrid systems verification, the approximations propagated by calculation and uncertainties on the parameters or on the initial conditions of a system can be computed using intervals-based computation. Since its conception, the automated deduction method known as tableau method has been extended with various axiomatic theories, none of them supporting intervals of floats. This study aims to explore to what extent can the tableau method be extended with an axiomatic theory of intervals, in order to take advantage for hybrid system verification. A first prover based on the tableau method for classical first-order logic has been created; the properties we wanted to describe on our intervals were then specified, and new inference rules were built and implemented on the initial prover. The final tool we get is able to prove first-order logic statements using equality, usual order on real numbers, and set membership and inclusion for closed bounded intervals.

Item Type:Thesis (PRE - Research Project)
Uncontrolled Keywords:Tableau method, automated deduction, intervals, logics, proofs
Subjects:Information and Communication Sciences and Technologies
ID Code:8071
Deposited By:Sadry CHEYNET-SOUBOU
Deposited On:08 janv. 2021 10:38
Dernière modification:08 janv. 2021 10:38

Repository Staff Only: item control page