Polarized Rewriting and Tableaux in B Set Theory

TL;DR

This paper extends the Zenon Modulo theorem prover with polarized rewriting for B Set Theory, aiming to improve automated reasoning on industrial benchmarks.

Contribution

It introduces polarized rewriting into Zenon Modulo and demonstrates its application to B Set Theory problems.

Findings

Enhanced theorem proving capabilities with polarized rewriting.

Successful application to industrial B Set Theory benchmarks.

Potential for improved reasoning efficiency.

Abstract

We propose and extension of the tableau-based first-order automated theorem prover Zenon Modulo to polarized rewriting. We introduce the framework and explain the potential benefits. The first target is an industrial benchmark composed of B Set Theory problems.