# Working with first-order proofs and provers

## TL;DR

This paper discusses developing tools to create a practical first-order logic proof environment, bridging the gap between automated and interactive proof systems for software correctness verification.

## Contribution

It introduces a work-in-progress set of tools designed to enable a usable first-order logic proof environment for software verification.

## Key findings

- Automated proof search tools predominantly use first-order logic.
- Interactive proof assistants typically employ higher-order logic.
- The proposed tools aim to unify proof environments for better software correctness verification.

## Abstract

Verifying software correctness has always been an important and complicated task. Recently, formal proofs of critical properties of algorithms and even implementations are becoming practical. Currently, the most powerful automated proof search tools use first-order logic while popular interactive proof assistants use higher-order logic. We present our work-in-progress set of tools that aim to eventually provide a usable first-order logic computer-assisted proof environment.