Proof Automation in the Theory of Finite Sets and Finite Set Relation Algebra

TL;DR

This paper introduces {log}-ITP, an interactive theorem prover integrating {log} for finite set theories, demonstrating significant proof automation and reduced proof complexity through empirical evaluation.

Contribution

It presents a prototype ITP that integrates {log} with existing systems, enhancing proof automation for finite set theories.

Findings

Noticeable reduction in proof size and complexity

Effective automation of many subgoals in finite set theorems

Empirical evaluation on 210 theorems shows improved proof efficiency

Abstract

{log} ('setlog') is a satisfiability solver for formulas of the theory of finite sets and finite set relation algebra (FSTRA). As such, it can be used as an automated theorem prover (ATP) for this theory. {log} is able to automatically prove a number of FSTRA theorems, but not all of them. Nevertheless, we have observed that many theorems that {log} cannot automatically prove can be divided into a few subgoals automatically dischargeable by {log}. The purpose of this work is to present a prototype interactive theorem prover (ITP), called {log}-ITP, providing evidence that a proper integration of {log} into world-class ITP's can deliver a great deal of proof automation concerning FSTRA. An empirical evaluation based on 210 theorems from the TPTP and Coq's SSReflect libraries shows a noticeable reduction in the size and complexity of the proofs with respect to Coq.