# Congress detail

**Authors**: Cristiá, Maximiliano; Rossi, Gianfranco; Frydman, Claudia.

**Title**: First steps in integrating {log} into Z/EVES.

**Resumen**: {log} is a Constraint Logic Programming language imple-menting a general theory of sets. As such it can determine the satisfi-ability of a large family of set formulas. Z/EVES is a proof assistantspecifically tailored for the Z notation. In turn, the Z notation is basedon a theory of sets. Hence, Z/EVES provides many facilities to provetheorems about set theory. We have observed that there are some suchtheorems that Z/EVES fails to prove automatically, while {log} is able todo it. Therefore, in this paper we propose to implement a new Z/EVESproof command by calling {log} after translating the goal to its inputlanguage. In this way it will be possible to prove many theorems auto-matically from Z/EVES.

**Meeting type**: Workshop.

**Type of job**: Artículo Completo.

**Production**: First steps in integrating {log} into Z/EVES.

**Scientific meeting**: 2nd International Workshop about Sets and Tools (SETS 2015).

**It's published?**: Yes

**Publication place**: Oslo

**Meeting month**: 6

**Year**: 2015.

**Link**: here