Tableaux Modulo Theories Using Superdeduction

TL;DR

This paper introduces a superdeduction-based tableau method for theories, integrated into Zenon, enabling automated verification of proof rules in set theory and first-order theories with demonstrated benchmarks.

Contribution

It presents a novel superdeduction approach for tableaux modulo theories within Zenon, extending its capabilities to verify proof rules in set theory and first-order theories.

Findings

Proposed a superdeduction tableau method integrated into Zenon.

Successfully verified proof rules from the B method database.

Extended Zenon to handle arbitrary first-order theories with benchmarks.

Abstract

We propose a method that allows us to develop tableaux modulo theories using the principles of superdeduction, among which the theory is used to enrich the deduction system with new deduction rules. This method is presented in the framework of the Zenon automated theorem prover, and is applied to the set theory of the B method. This allows us to provide another prover to Atelier B, which can be used to verify B proof rules in particular. We also propose some benchmarks, in which this prover is able to automatically verify a part of the rules coming from the database maintained by Siemens IC-MOL. Finally, we describe another extension of Zenon with superdeduction, which is able to deal with any first order theory, and provide a benchmark coming from the TPTP library, which contains a large set of first order problems.