The crisis in finite mathematics: automated reasoning as cause and cure. (English) Zbl 1433.68566
Bundy, Alan (ed.), Automated deduction – CADE-12. 12th international conference, Nancy, France, June 26 – July 1, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 814, 1-13 (1994).
For the entire collection see [Zbl 0875.00063].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 03B35 | Mechanization of proofs and logical operations |
| 20N05 | Loops, quasigroups |
Software:
SATCHMOReferences:
| [1] | K. Appel & W Haken, Proof of the 4-Color Theorem, Discrete Mathematics, 16 (1977), pp. 179-180. · Zbl 0339.05109 |
| [2] | B. Benhamou & L. Sais, Theoretical Study of Symmetries in Propositional Calculus and Applications, Proc. 11th International Conference on Automated Deduction (1992), pp. 281-294. · Zbl 0925.03077 |
| [3] | F. Bennett & L. Zhu, Conjugate-Orthogonal Latin Squares and Related Structures, Contemporary Design Theory: A Collection of Surveys, ed. J. Dinitz & D. Stinson, New York, Wiley, 1992. |
| [4] | M. Fujita, J. Slaney & F. Bennett, Automatic Generation of Some Results in Finite Algebra, Proc. 13th International Joint Conference on Artificial Intelligence (1993), pp. 52-57. |
| [5] | G. Kolata, Computers Still Can’t Do Beautiful Mathematics, New York Times, Week in Review §E, Sunday, July 14, 1991, p.4. |
| [6] | C. W. H. Lam, L. Thiel & S. Swiercz, The Non-existence of Finite Projective Planes of Order 10, Canadian Journal of Mathematics 41 (1989), pp. 1117-1123. · Zbl 0691.51003 |
| [7] | A. Mackworth, Constraint Satidfaction, Encyclopedia of Artificial Intelligence (ed. Shapiro) 1987, pp. 205-211. |
| [8] | R. Manthey & F. Bry, SATCHMO: A Theorem Prover Implemented in Prolog, Proc. 9th International Conference on Automated Deduction (1988), pp 415-434. · Zbl 0668.68104 |
| [9] | B. McKay & S. Radziszowski, R(4, 5) = 25, Journal of Graph Theory, forthcoming. |
| [10] | J. Horgan, The Death of Proof, Scientific American, 237.4 (October 1993), pp. 74-82. |
| [11] | J. Slaney, M. Stickel & M. Fujita, Automated Reasoning and Exhaustive search: Quasigroup Existence Problems, Journal of Computers in Mathematics with Applications, special issue on Automated Reasoning, forthcoming. · Zbl 0827.20083 |
| [12] | H. |
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.
