# Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa"

## TL;DR

The paper introduces iapa, a new tool integrated with Atelier B, enabling users to simplify proof obligations and automatically dispatch them to theorem provers, improving formal method efficiency.

## Contribution

It presents iapa, a novel interface that streamlines proof obligation management and automatic theorem prover integration within Atelier B.

## Key findings

- iapa successfully simplifies proof obligations
- Automated dispatch to theorem provers enhances proof efficiency
- Improves usability of formal verification tools

## Abstract

The application of automatic theorem provers to discharge proof obligations is necessary to apply formal methods in an efficient manner. Tools supporting formal methods, such as Atelier~B, generate proof obligations fully automatically. Consequently, such proof obligations are often cluttered with information that is irrelevant to establish their validity. We present iapa, an "Interface to Automatic Proof Agents", a new tool that is being integrated to Atelier~B, through which the user will access proof obligations, apply operations to simplify these proof obligations, and then dispatch the resulting, simplified, proof obligations to a portfolio of automatic theorem provers.