Cantone, Domenico; Ferro, Alfredo Techniques of computable set theory with applications to proof verification. (English) Zbl 0852.03004 Commun. Pure Appl. Math. 48, No. 9-10, 901-945 (1995). Reviewer: J.M.Plotkin (East Lansing) MSC: 03B25 03E99 03B35 PDFBibTeX XMLCite \textit{D. Cantone} and \textit{A. Ferro}, Commun. Pure Appl. Math. 48, No. 9--10, 901--945 (1995; Zbl 0852.03004) Full Text: DOI
Ferro, A. Decision procedures for elementary sublanguages of set theory: XII. Multilevel syllogistic extended with singleton and choice operators. (English) Zbl 0734.03005 J. Autom. Reasoning 7, No. 2, 257-270 (1991). MSC: 03B25 03E99 03B35 68T15 PDFBibTeX XMLCite \textit{A. Ferro}, J. Autom. Reasoning 7, No. 2, 257--270 (1991; Zbl 0734.03005)
Cantone, Domenico; Ferro, Alfredo; Omodeo, Eugenio Computable set theory. Vol. 1. (English) Zbl 0755.03024 International Series of Monographs on Computer Science. 6. Oxford: Univ. Press. XII, 347 p. (1989). Reviewer: J.M.Plotkin (East Lansing) MSC: 03E30 03B25 03-02 PDFBibTeX XMLCite \textit{D. Cantone} et al., Computable set theory. Vol. 1. Oxford: Univ. Press (1989; Zbl 0755.03024)
Ferro, Alfredo; Sorace, Giuseppe; Schwartz, Jacob T. A note on extending decision algorithms by stable predicates. (English) Zbl 0708.03005 Matematiche 43, No. 1-2, 297-302 (1988). MSC: 03B25 03B35 03E99 PDFBibTeX XMLCite \textit{A. Ferro} et al., Matematiche 43, No. 1--2, 297--302 (1988; Zbl 0708.03005)
Cantone, D.; Ferro, A.; Omodeo, E. G. Decision procedures for elementary sublanguages of set theory. VIII. A semidecision procedure for finite satisfiability of unquantified set- theoretic formulae. (English) Zbl 0645.03007 Commun. Pure Appl. Math. 41, No. 1, 105-120 (1988). Reviewer: J.M.Plotkin MSC: 03B25 03E99 PDFBibTeX XMLCite \textit{D. Cantone} et al., Commun. Pure Appl. Math. 41, No. 1, 105--120 (1988; Zbl 0645.03007) Full Text: DOI
Cantone, D.; Ferro, A. Some recent decidability results in set theory. (English) Zbl 0667.03007 Atti degli incontri di logica matematica, Vol. 3, Siena & Padova/Italia 1985/86, 383-387 (1987). Reviewer: A.Pettorossi MSC: 03B25 03E99 PDFBibTeX XML
Ferro, A.; Omodeo, E. G. Decision procedures for elementary sublanguages of set theory. VII: Validity in set theory when a choice operator is present. (English) Zbl 0656.03007 Commun. Pure Appl. Math. 40, No. 3, 265-280 (1987). Reviewer: J.M.Plotkin MSC: 03B25 03E99 PDFBibTeX XMLCite \textit{A. Ferro} and \textit{E. G. Omodeo}, Commun. Pure Appl. Math. 40, No. 3, 265--280 (1987; Zbl 0656.03007) Full Text: DOI Link
Cantone, D.; Ferro, A.; Omodeo, E.; Schwartz, J. T. Decision algorithms for some fragments of analysis and related areas. (English) Zbl 0656.03006 Commun. Pure Appl. Math. 40, No. 3, 281-300 (1987). Reviewer: J.M.Plotkin MSC: 03B25 PDFBibTeX XMLCite \textit{D. Cantone} et al., Commun. Pure Appl. Math. 40, No. 3, 281--300 (1987; Zbl 0656.03006) Full Text: DOI Link
Cantone, D.; Ferro, A.; Schwartz, J. T. Decision procedures for elementary sublanguages of set theory. V. Multilevel syllogistic extended by the general union operator. (English) Zbl 0634.03008 J. Comput. Syst. Sci. 34, 1-18 (1987). Reviewer: J.M.Plotkin MSC: 03B25 03E99 03B30 PDFBibTeX XMLCite \textit{D. Cantone} et al., J. Comput. Syst. Sci. 34, 1--18 (1987; Zbl 0634.03008) Full Text: DOI
Cantone, Domenico; Ferro, Alfredo; Sorace, Giuseppe; Micale, Biagio Decision procedures for elementary sublanguages of set theory. IV: Formulae involving a rank operator or one occurrence of \(\Sigma (x)=\{\{y\}|\) y\(\in x\}\). (English) Zbl 0595.03007 Commun. Pure Appl. Math. 40, No. 1, 37-77 (1987). MSC: 03B25 03E99 PDFBibTeX XMLCite \textit{D. Cantone} et al., Commun. Pure Appl. Math. 40, No. 1, 37--77 (1987; Zbl 0595.03007) Full Text: DOI
Ferro, A. A note on the decidability of MLS extended with the powerset operator. (English) Zbl 0586.03007 Commun. Pure Appl. Math. 38, 367-374 (1985). Reviewer: M.Tetruašvili MSC: 03B25 03E30 PDFBibTeX XMLCite \textit{A. Ferro}, Commun. Pure Appl. Math. 38, 367--374 (1985; Zbl 0586.03007) Full Text: DOI
Cantone, D.; Schwartz, J. T.; Ferro, A. Decision procedures for elementary sublanguages of set theory. VI: Multi- level syllogistic extended by the powerset operator. (English) Zbl 0582.03005 Commun. Pure Appl. Math. 38, 549-571 (1985). Reviewer: J.M.Plotkin MSC: 03B25 03E99 PDFBibTeX XMLCite \textit{D. Cantone} et al., Commun. Pure Appl. Math. 38, 549--571 (1985; Zbl 0582.03005) Full Text: DOI Link
Breban, Michael; Ferro, Alfredo Decision procedures for elementary sublanguages of set theory. III: Restricted classes of formulas involving the power set operator and the general set union operator. (English) Zbl 0542.03003 Adv. Appl. Math. 5, 147-215 (1984). Reviewer: J.M.Plotkin MSC: 03B25 03E99 PDFBibTeX XMLCite \textit{M. Breban} and \textit{A. Ferro}, Adv. Appl. Math. 5, 147--215 (1984; Zbl 0542.03003) Full Text: DOI
Breban, M.; Ferro, A.; Omodeo, E. G.; Schwartz, J. T. Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions. (English) Zbl 0465.03003 Commun. Pure Appl. Math. 34, 177-195 (1981). MSC: 03B25 03E99 PDFBibTeX XMLCite \textit{M. Breban} et al., Commun. Pure Appl. Math. 34, 177--195 (1981; Zbl 0465.03003) Full Text: DOI
Ferro, A.; Omodeo, E. G.; Schwartz, J. T. Decision procedures for some fragments of set theory. (English) Zbl 0457.03009 Automated deduction, 5th Conf., Les Arcs/France 1980, Lect. Notes Comput. Sci. 87, 88-96 (1980). MSC: 03B25 03B30 PDFBibTeX XML
Ferro, Alfredo; Omodeo, Eugenio G.; Schwartz, Jacob T. Decision procedures for elementary sublanguages of set theory. I: Multi- level syllogistic and some extensions. (English) Zbl 0453.03009 Commun. Pure Appl. Math. 33, 599-608 (1980). MSC: 03B25 03E99 PDFBibTeX XMLCite \textit{A. Ferro} et al., Commun. Pure Appl. Math. 33, 599--608 (1980; Zbl 0453.03009) Full Text: DOI
Ferro, Alfredo; Omodeo, Eugenio G. An efficient validity test for formulae in extensional two-level syllogistic. (English) Zbl 0448.68021 Matematiche 33, 130-137 (1978). MSC: 68T15 03B25 03-04 03B35 68N99 PDFBibTeX XMLCite \textit{A. Ferro} and \textit{E. G. Omodeo}, Matematiche 33, 130--137 (1978; Zbl 0448.68021)