×

Towards the automation of set theory and its logic. (English) Zbl 0395.68082


MSC:

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

Citations:

Zbl 0193.304
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Quine, W. V. O., Set Theory and its Logic; Quine, W. V. O., Set Theory and its Logic
[2] Brown, F. M., Doing arithmetic without diagrams, DAI Research Report No. 16a, To appear in Artificial Intelligence; Brown, F. M., Doing arithmetic without diagrams, DAI Research Report No. 16a, To appear in Artificial Intelligence · Zbl 0359.68108
[3] Morse, Anthony P., (A Theory of Sets (1965), Academic Press: Academic Press London) · Zbl 0179.01502
[4] Bledsoe, W. W., Splitting and reduction heuristics in automatic theorem proving, Artificial Intelligence, 2, 1 (1971) · Zbl 0221.68052
[5] Bledsoe, W. W.; Boyer, R. S.; Henneman, W. H., Computer proofs of limit theorems, Artificial Intelligence, 3 (1972) · Zbl 0242.68055
[6] Boyer, Robert S.; Strother Moore, J., Proving Theorems about LISP functions, (IJCA13 Proceedings (1973)) · Zbl 0338.68014
[7] Strother Moore, J., Computational logic: Structure sharing and proof of program properties, part II, DCL Memo No. 68.; Strother Moore, J., Computational logic: Structure sharing and proof of program properties, part II, DCL Memo No. 68.
[8] Aubin, R., Mechanizing structural induction, (Ph.D. Thesis (1976), Department of Artificial Intelligence: Department of Artificial Intelligence University of Edinburgh) · Zbl 0423.68051
[9] McCarthy, J., (LISP 1.5 Programming Manual (1965), M.I.T. Press: M.I.T. Press Cambridge, MA)
[10] Wang, Hao, Toward mechanical mathematics, IBM Journal of Research and Development, 4, 2-22 (1960) · Zbl 0097.00404
[11] Prawitz, D., An improved proof procedure, Theoria, 26, 102-139 (1960) · Zbl 0099.00801
[12] Robinson, J. A., A machine-oriented logic based on the resolution principle, J.A.C.M., 12, 23-41 (January 1965) · Zbl 0139.12303
[13] Bibel, W.; Schreiber, J., Proof search in a Gentzen-like system of first order logic, (International Computing Symposium (1975), North-Holland Publishing Company: North-Holland Publishing Company Amsterdam) · Zbl 0324.68053
[14] Siekmann, J., A modification of the unification algorithm in automatic theorem proving, (Masters Thesis (1972), University of Essex)
[15] Plotkin, G., Building in equational theories, Machine Intelligence, 7 (1972) · Zbl 0262.68036
[16] Lankford, Dallas S., Canonical algebraic simplification, (Maths Department Memo ATP-25 (May 1975), University of Texas at Austin)
[17] Hayes, Pat, A Logic of Action, Machine Intelligence, 6 (1971)
[18] Quam, Lynn, Stanford AT LISP 1.6 Manual; Quam, Lynn, Stanford AT LISP 1.6 Manual
[19] Bebrow, R. et al., UCI LISP Manual; Bebrow, R. et al., UCI LISP Manual
[20] Pastre, D., Demonstration Automatique de Theoremes en Theorie des Ensembles, These de de 3eme cycle (1976), Paris VI
[21] Pastre, D., Automatic theorem proving in set theory (1977), University of Paris VI · Zbl 0374.68059
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.