Exploratory integration of an oracle for mathematical functions in tableau method

January 23, 2023

François Pessaux (U2IS, ENSTA Paris)

The tableaux method is an automated proof search technics initially dealing with first-order logics. Many extensions have been proposed to accommodate different logics and additional theories. Toward the hope to extend this method with guaranteed simulation to prove properties on hybrid systems dynamics described by ODEs, we start with a more modest targe. We present the integration of tableaux to standard arithmetic equations. We show how an oracle can be used to deal with formula involving membership to constant intervals.