École Nationale Supérieure de
Techniques Avancées

Abstract

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.