We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Proof Automation in the Theory of Finite Sets and Finite Set Relation Algebra.
- Authors
Cristiá, Maximiliano; Katz, Ricardo D; Rossi, Gianfranco
- 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.
- Subjects
RELATION algebras; SET theory; PROOF theory; FINITE, The
- Publication
Computer Journal, 2022, Vol 65, Issue 7, p1891
- ISSN
0010-4620
- Publication type
Article
- DOI
10.1093/comjnl/bxab030