Decision procedures for elementary sublanguages of set theory. I: Multi- level syllogistic and some extensions. (English) Zbl 0453.03009


03B25 Decidability of theories and sets of sentences
03E99 Set theory
Full Text: DOI


[1] Behmann, Math. Annalen 86 pp 163– (1922)
[2] Davis, J. Appl. Comput. Math. 7 pp 201– (1960)
[3] Aristotle’s Syllogistic, Clarendon Press, Oxford, 1952.
[4] and , A simplifier based on efficient decision algorithms, Fifth Ann. Symp. on Principles of Programming Languages, 1978, pp. 141–150.
[5] Complexity of combinations of quantifier-free procedures, Workshop on Automatic Deduction, Austin, Texas, 1979.
[6] On specifying verifiers, Proc. of Conf. on Principles of Programming Languages, ACM, New York City, 1979, pp. 106–116.
[7] Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt, Comptes-rendus du premiere Congres des Mathematicien des Pays Slaves, Warsaw, 1930, pp. 92–101. · JFM 56.0825.04
[8] Methods of Logic, Henry Holt, New York, 1950.
[9] Instantiation and decision procedures for certain classes of quantified set-theoretic formulae, Inst. for Computer Appl. in Science and Engineering, NASA Langley Research Center, Hampton, VA, Report #7810, 1978.
[10] A survey of program proof technology, Courant Institute, Computer Science Dept., Report #1, September 1978.
[11] Shepherdson, J. Symbolic Log. 21 pp 137– (1956)
[12] Ordinal Algebras, North Holland, New York, 1956.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.