| dc.creator | Cristía, Maximiliano | |
| dc.creator | Rossi, Gianfranco | |
| dc.date | 2022-10 | |
| dc.date | 2022 | |
| dc.date | 2023-04-18T15:31:32Z | |
| dc.date.accessioned | 2023-07-15T10:11:52Z | |
| dc.date.available | 2023-07-15T10:11:52Z | |
| dc.identifier | http://sedici.unlp.edu.ar/handle/10915/151644 | |
| dc.identifier | https://publicaciones.sadio.org.ar/index.php/JAIIO/article/download/302/251 | |
| dc.identifier | issn:2451-7496 | |
| dc.identifier.uri | https://repositorioslatinoamericanos.uchile.cl/handle/2250/7490953 | |
| dc.description | Formal reasoning about finite sets and cardinality is important for many applications, including software verification, where very often one needs to reason about the size of a given data structure. The Constraint Logic Programming tool {log} (‘setlog’) provides a decision procedure for deciding the satisfiability of formulas involving very general forms of finite sets, although it does not provide cardinality constraints. In this paper we adapt and integrate a decision procedure for a theory of finite sets with cardinality into {log}. The proposed solver is proved to be a decision procedure for its formulas. Besides, the new CLP instance is implemented as part of the {log} tool. In turn, the implementation uses Howe and King’s Prolog SAT solver and Prolog’s CLP(Q) library, as an integer linear programming solver. The empirical evaluation of this implementation based on +250 real verification conditions shows that it can be useful in practice. | |
| dc.description | Sociedad Argentina de Informática e Investigación Operativa | |
| dc.format | application/pdf | |
| dc.format | 70-70 | |
| dc.language | en | |
| dc.rights | http://creativecommons.org/licenses/by-nc-sa/4.0/ | |
| dc.rights | Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC BY-NC-SA 4.0) | |
| dc.subject | Ciencias Informáticas | |
| dc.subject | Constraint Logic Programming tool | |
| dc.subject | Theory of finite sets | |
| dc.title | Integrating cardinality constraints into constraint logic programming with sets | |
| dc.type | Objeto de conferencia | |
| dc.type | Resumen | |
