Proof Automation in the Theory of Finite Sets and Finite Set Relation Algebra
share
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.
READ FULL TEXT