English version:
============================================
The axioms ZFC of Zermelo-Fraenkel form an infinite collection, due to the presence of one or two axioms schemes (separation and replacement). This makes it impossible to exploit directly theorem-provers such as Otter, because the specific instances of separation and replacement which enter into play in getting a desired proof must be, every time, singled out and introduced explicitly as user axioms.

Even if we adopted a finite system of axioms (for example by resorting to the Goedel-Bernays theory VBG instead of to ZFC), it would be necessary to formulate the axioms in a way different from the one most widely adopted in the scientific literature: in fact, the way in which axioms are stated is crucial to ensure the effectiveness of the automatic proof process (see [B*86], later resumed and improved by [Qua92]).

Here we will content ourselves to formulate the unproblematic part (unproblematic insofar as finitely axiomatizable) of the theory ZFC, leaving separation and replacement out of our consideration. Some sophistication, in our axiomatic formulation, results from our willingness to subdivide notions across different conceptual plans (the Boolean level, the extensionality axiom, and so on up to the infinity and choice axioms).

%============================================
Otter files containing axioms:

• "Breadth" of membership
• "Depth of membership
• Extensionality, part 1
• Extensionality, part 2
• Regularity
• Powerset
• Transitive closure
• Unionset
• The most controversial postulate of set theory, the Axiom of Choice
• Infinity
• Finiteness (Antithetic to the infinity postulate)

• "Correctness" of JTS' pairing notion

%%INCLUDE ALL ITEMS SAVE fty

Italian version:
%============================================
Gli assiomi ZFC di Zermelo-Fraenkel formano una collezione infinita, per via della presenza di uno o due schemi di assioma (separazione e rimpiazzamento). Questo rende impossibile un'impiego diretto di dimostratori quali Otter, nel senso che le istanze particolari di separazione e rimpiazzamento utili ai fini di una dimostrazione devono essere, volta per volta, individuate e introdotte esplicitamente come assiomi dall'utente.

Anche se adottassimo un sistema finito di assiomi (ad esempio prescegliendo la teoria VBG di Goedel-Bernays alla ZFC), sarebbe necessario formulare gli assiomi in maniera diversa da quella piu` affermata in letteratura, poiche` il modo in cui gli assiomi sono espressi e` determinante per l'efficacia del processo di dimostrazione automatica (vedi [B*86], successivamente ripreso e perfezionato da [Qua92]).

Qui ci contentiamo di formulare la parte non problematica (in quanto finitamente assiomatizzabile) di ZFC, lasciando fuori separazione e rimpiazzamento; tuttavia la formulazione degli assiomi puo` apparire piu` complessa del necessario, in quanto essa mira a suddividere le nozioni su piani diversi (il livello booleano, l'assioma di estensionalita` e via via fino agli assiomi di infinita` e scelta).

%============================================

%%INCLUDERE TUTTI I PEZZI AD ECCEZIONE DI fty