CIFASIS   20631
CENTRO INTERNACIONAL FRANCO ARGENTINO DE CIENCIAS DE LA INFORMACION Y DE SISTEMAS
Unidad Ejecutora - UE
artículos
Título:
Proof Automation in the Theory of Finite Sets and Finite Set Relation Algebra
Autor/es:
ROSSI, GIANFRANCO; CRISTIÁ, MAXIMILIANO; KATZ, RICARDO D
Revista:
COMPUTER JOURNAL
Editorial:
OXFORD UNIV PRESS
Referencias:
Año: 2021
ISSN:
0010-4620
Resumen:
{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.