# Automated Formal Proofs for Polynomial and Transcendental Problems

Lead Research Organisation:
University of Cambridge

Department Name: Computer Science and Technology

### Abstract

Many applications in science and engineering involve mathematical formulas. Such formulas may involve polynomials, logarithms, exponentials and related functions, perhaps combined using logical symbols to express conditional statements. No automatic procedure exists for solving such problems in the general case. Where automatic procedures do exist, they are often far too expensive (in terms of computer time and memory requirements) to use in practice. However, a judicious selection of specialised procedures can yield efficient solutions for many problems that arise in practice. The proposal is to identify and implement variety of such procedures.This work will be undertaken in the context of software tools known as interactive theorem provers. These tools perform logical deductions to be very high degree of reliability; they are increasingly being utilised to help assure correctness for safety critical applications. A primary challenge of this project is to reconcile the detailed low-level checking used in interactive theorem provers with the high-level reasoning typical of most approaches to solving mathematical formulas. One fruitful technique is to deliver evidence from the mathematical solver to the interactive theorem prover: for some types of problems, finding the solution is difficult, but verifying a claimed solution is easy.

### Organisations

### Publications

Akbarpour B
(2009)

*MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions*in Journal of Automated Reasoning
Chaieb A
(2010)

*Formal Power Series*in Journal of Automated Reasoning
Da Silva L
(2023)

*Antibacterial potential of chalcones and its derivatives against Staphylococcus aureus.*in 3 Biotech
Denman W
(2009)

*Formal verification of analog designs using MetiTarski*Description | The purpose of this one-year project was to deliver specialised algorithmic support for problems involving polynomials and transcendental functions. The general case being intractable, the point was to identify and solve important special cases. The outcome consisted largely of code, added to the Isabelle theorem prover, for deciding important classes of arithmetic problems. An additional outcome is an Isabelle theory of formal power series, which provides a basis for formalising approximations to transcendental functions. |

Exploitation Route | The code and formal theories developed within this project has been incorporated into Isabelle, which is freely available and used worldwide, in both academic and industrial research environments. |

Sectors | Digital/Communication/Information Technologies (including Software) |

Title | Arithmetic decision procedures in Isabelle |

Description | A primary goal of this project was to investigate advanced mathematical procedures for simplifying and solving difficult problems using a combination of techniques. The project's main outputs consisted of advanced arithmetic decision procedures (that is, automatic problem solvers) that were incorporated into Isabelle, an interactive theorem prover. |

Type Of Technology | Software |

Year Produced | 2009 |

Open Source License? | Yes |

Impact | This software is an integral part of Isabelle, which is used worldwide. |