Tags:Euclidean geometry, formal reasoning and modelling dynamic systems
Abstract:
We report on a specific reachability problem which asks to find one-dimensional functions along the faces of a collection of cubes in three-dimensional Euclidean real space that respect certain local monotonicity criteria and certain global connectivity properties. The motivation for this problem is drawn from efforts to provide the background technology that is necessary to digitalise simple experiments in natural sciences' school classes. In particular, we aim to provide methods of logical reasoning which determine the correctness of statements about the way that variables influence each other in such experiments. Here we focus on situations in which two variables influence a third one: for example temperature and pressure influence the volume of a gas. Solving the aforementioned problem about the existence of a web of one-dimensional functions in three-dimensional space turns out to be the key to completeness and to an algorithmic approach in a calculus for reasoning about such situations.