Automatic theorem proving in set theory. (English) Zbl 0374.68059


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03Exx Set theory
03-04 Software, source code, etc. for problems pertaining to mathematical logic and foundations
Full Text: DOI


[1] (Abadie, J., Integer and Nonlinear Programming (1970), American Elsevier: American Elsevier New York) · Zbl 0321.00011
[2] Brown, F. M., Doing arithmetic without diagrams, Artificial Intelligence, 8, 179-200 (1977) · Zbl 0359.68108
[3] Brown, F. M., Towards the automation of set theory and its logic, Submitted to Artificial Intelligence; Brown, F. M., Towards the automation of set theory and its logic, Submitted to Artificial Intelligence · Zbl 0395.68082
[4] Halmos, P. R., Notice Set Theory (1960), Van Nostrand: Van Nostrand Princeton · Zbl 0117.10502
[5] Barachen, L.; Wos, L., Unit refutations and born sets, J. ACM, 21, 590-605 (1974) · Zbl 0296.68093
[6] Brivise, J. L., Theorie Axiomatique des Ensembles (1969), P.U.F.: P.U.F. Paris · Zbl 0175.00601
[7] Newma, A. J., A relaxation approach to splitting in an automatic theorem prover, Artificial Intelligence, 6, 25-39 (1975) · Zbl 0301.68087
[8] Nevis, A. J., Plane geometry theorem proving using forward chaining, Artificial Intelligence, 6, 1-23 (1975) · Zbl 0301.68086
[9] Petersen, G. E., Theorem proving with lemmas, J. ACM, 23, 573-581 (1976) · Zbl 0333.68061
[10] Sigler, L. E., Exercises in Set Theory (1966), Van Nostrand: Van Nostrand London · Zbl 0144.24803
[11] Slogle, J. E., Automatic theorem proving with built-in theories including equality, partial ordering and sets, J. ACM, 19, 120-135 (1972) · Zbl 0231.68035
[12] Slagla, J. R.; Norton, J. M., Experiments with an automatic theorem-prover having partial ordering inference rules, C. ACM, 16, 682-688 (1973) · Zbl 0271.68062
[13] Slagla, J. R.; Norton, J. M., Automated theorem proving for the theories of partial and total ordering, Computer Journal, 18, 49-54 (1973) · Zbl 0296.68091
[14] Wang, H., Towards mechanical mathematics, IBM Journal of Research and Development, 4, 2-22 (1960)
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.