Proof Automation in the Theory of Finite Sets and Finite Set Relation Algebra. (3rd May 2021)

• Record Type: Journal Article
• Authors: Cristiá, Maximiliano; Katz, Ricardo D; Rossi, Gianfranco
• Is Part Of: Computer journal. Volume 65:Number 7(2022)
• Page Start: 1891
• Page End: 1903
• Publication Date: 2021-05-03
• Subjects: {log} -- set theory -- automated proofs -- constraint logic programming; Computers -- Periodicals; 005.1
• DOI: 10.1093/comjnl/bxab030
• Languages: English
• ISSNs: 0010-4620

Abstract

Abstract: $\{log\}$ ('setlog') is a satisfiability solver for formulas of the theory of finite sets and finite set relation algebra (FS&RA). As such, it can be used as an automated theorem prover for this theory. $\{log\}$ is able to automatically prove a number of FS&RA 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 FS&RA. 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.