Automatic Proof Procedures for Polynomials and Special Functions

An engineering design is expected to satisfy safety constraints, many of which can be expressed as mathematical and logical formulas. Computer software exists that can check some such formulas automatically, but although they can have a large and complicated logical structure, the mathematical component currently has to be linear: in other words, involving nothing more complicated than addition. Real-world engineering problems involve sophisticated mathematical concepts, such as polynomials and transcendental functions.The investigators have developed software (called MetiTarski and RAHD) that can solve such problems in many cases. The current project will extend the scope of this software, increasing its power and targeting it at specific real-world application areas. One such application is analogue circuitry, which is widespread in consumer electronics. The project will investigate many other potential applications In engineering and the mathematical sciences.

Who will benefit from this research? The project will deliver two open-source pieces of mathematical software: MetiTarski and RAHD. MetiTarski has potential applications throughout the engineering sector, and possibly in financial mathematics. RAHD will be a component of MetiTarski, and it also has scientific applications in its own right. The main target beneficiaries are engineering firms and particularly those devoted to high integrity systems. Both software tools also have potential applications to university mathematics teaching. How will they benefit from this research? MetiTarski has the potential to be useful in the design of hybrid and control systems, analogue circuits, and other areas of engineering that rely on differential equations or real valued special functions. Engineering firms may be able to design products more cheaply than before, conferring economic benefits. These products may also be safer than before, when simulation is replaced or supplemented by formal proof; therefore, a further benefit is enhanced public safety. What will be done to ensure that they benefit from this research? The project is designed from the outset to target the development of MetiTarski on the needs of potential users. We shall engage with experts from various industrial sectors to obtain problems and test data. In this way, limitations of MetiTarski and RAHD will be identified and addressed. We shall visit our engineering experts to exchange results. We shall present findings and demonstrate our software at conferences frequented by industrialists, in addition to the usual academic conferences. We shall also strive to make our software robust, well-documented and easy to use. We have a good track record with regard to Isabelle, which now has users across the developed world.