Fetching the paper…
Reading the bibliography…
This paper describes a program that solves elementary mathematical problems, mostly in metric space theory, and presents solutions that are hard to distinguish from solutions that might be written by human mathematicians.
Cambridge University Press (1910)
Whitehead, A., Russell, B.: Principia Mathematica · 1910
Earlier work this paper cites.
Oxford University Press (1954)
Polya, G.: Mathematics and plausible reasoning, Vol 1: Induction and analogy in mathematics · 1954
Earlier work this paper cites.
Oxford University Press (1954)
Polya, G.: Mathematics and plausible reasoning, Vol 2: Patterns of plausible inference · 1954
Earlier work this paper cites.
IRE Transactions of information theory 2-3
Newell, A., Simon, H.A.: The logic theory machine: A complex information processing system · 1956
Earlier work this paper cites.
Pólya, G.: How to solve it: A new aspect of mathematical method (1957)
1957
Earlier work this paper cites.
Rand Corporation (1959)
Newell, A., Shaw, J.C., Simon, H.A.: Report on a General Problem-solving Program · 1959
Earlier work this paper cites.
Artificial Intelligence 2
Bledsoe, W.W.: Splitting and reduction heuristics in automatic theorem proving · 1971
Earlier work this paper cites.
In: Proceedings of the third annual ACM symposium on Theory of computing, pp. 151–158. ACM (1971)
Cook, S.A.: The complexity of theorem-proving procedures · 1971
Earlier work this paper cites.
Artificial Intelligence 3
Bledsoe, W.W., Boyer, R.S., Henneman, W.H.: Computer proofs of limit theorems · 1972
Earlier work this paper cites.
Springer (1972)
Karp, R.M.: Reducibility among Combinatorial Problems · 1972
Earlier work this paper cites.
Prentice-Hall, Englewood Cliffs, NJ (1972)
Newell, A., Simon, H.A.: Human Problem Solving · 1972
Earlier work this paper cites.
In: IJCAI-4, Tbilissi, Georgien, 3-8 Sep. 1975, Proceedings, pp. 22–28 (1975)
Bundy, A.: Analysing mathematical proofs · 1975
Earlier work this paper cites.
In: P. Cole, J.L. Morgan (eds.) Syntax and Semantics, vol. 3, pp. 41–58. Academic Press, New York (1975)
Grice, H.P.: Logic and conversation · 1975
Earlier work this paper cites.
IEEE Transactions on Computers 100
Reiter, R.: A semantically guided deductive system for automatic theorem proving · 1976
Earlier work this paper cites.
Artificial Intelligence 9
Bledsoe, W.W.: Non-resolution theorem proving · 1977
Earlier work this paper cites.
In: Proceedings of the 5th international joint conference on Artificial intelligence-Volume 1, pp. 501–510. Morgan Kaufmann Publishers Inc. (1977)
Bledsoe, W.W.: Set variables · 1977
Cited alongside, same era.
Journal of the ACM 24
Bledsoe, W.W., Ballantyne, A.M.: Automatic proofs of theorems in analysis using nonstandard techniques · 1977
Cited alongside, same era.
Academic Press, New York (1979)
Boyer, R.S., Moore, J.S.: A Computational Logic · 1979
Cited alongside, same era.
Springer (1979)
Gordon, M.J., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation, Lecture Notes in Computer Science , vol. 78 · 1979
Cited alongside, same era.
In: Proc. of IJCAI, vol. 83, pp. 892–901 (1983)
Bledsoe, W.W.: Using examples to generate instantiations for set variables · 1983
Cited alongside, same era.
Academic Press (1983)
Bundy, A.: The computer modelling of mathematical reasoning · 1983
Cited alongside, same era.
Mathware & soft computing 3
Cordeschi, R.: The role of heuristics in automated theorem proving – J.A. Robinson’s resolution principle · 1996
Later among the works it cites.
Ph.D. thesis, University of Edinburgh (1996)
Knott, A.: A data-driven methodology for motivating a set of coherence relations · 1996
Later among the works it cites.
Journal of Automated Reasoning 19
McCune, W.: Solution of the robbins problem · 1997
Later among the works it cites.
In: W. Bibel, P.H. Schmitt (eds.) Automated Deduction: A Basis for Applications. Volume III, Applications”, pp. 77–95. Kluwer Academic Publishers (1998)
Kerber, M.: Proof planning: A practical approach to mechanized reasoning in mathematics · 1998
Later among the works it cites.
Strategies in Automated Deduction (STRATEGIES’99) p. 17 (1999)
Bundy, A.: A critique of proof planning · 1999
Later among the works it cites.
In: Artificial Intelligence Today, pp. 153–174. Springer-Verlag (1999)
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Academic Press (1983)
Bundy, A.: The Computer Modelling of Mathematical Reasoning · 1983
Cited alongside, same era.
Journal of Experimental Psychology: General 112
Sweller, J., Mawer, R.F., Ward, M.R.: Development of expertise in mathematical problem solving · 1983
Cited alongside, same era.
In: Proceedings of the IJCAI-85, 1985, pp. 1221–1230 (1985)
Bundy, A.: Discovery and reasoning in mathematics · 1985
Cited alongside, same era.
Journal of Educational Psychology 77
Owen, E., Sweller, J.: What do students learn while solving mathematics problems? · 1985
Cited alongside, same era.
Journal of Automated Reasoning 1
Wos, L., Pereira, F., Hong, R., Boyer, R.S., Moore, J.S., Bledsoe, W.W., Henschen, L., Buchanan, B.G., Wrightson, G., Green, C.: An overview of automated reasoning and related fields · 1985
Cited alongside, same era.
Tech. Rep. MS-CIS-88-17, University of Pennsylvania (1987)
Felty, A., Miller, D.: Proof explanation and revision · 1987
Cited alongside, same era.
Bundy, A.: A survey of automated deduction · 1999
Later among the works it cites.
In: Proceedings of Sixteenth National Conference on Artificial Intelligence, pp. 277–284 (1999)
Holland-Minkley, A.M., Barzilay, R., Constable, R.L.: Verbalization of high-level formal proofs · 1999
Later among the works it cites.
Cambridge University Press (2000)
Reiter, E., Dale, R.: Building natural language generation systems · 2000
Later among the works it cites.
MIT Press (2001)
MacKenzie, D.: Mechanizing Proof · 2001
Later among the works it cites.
In: V. Diekert, M. Volkov, A. Voronkov (eds.) Proceedings of the 2nd International Computer Science Symposium in Russia, no. 4649 in Lecture Notes in Computer Science, pp. 7–23. Springer-Verlag (2007)
Sutcliffe, G.: TPTP, TSTP, CASC, etc · 2007
Later among the works it cites.
Cambridge University Press (2009)
Harrison, J.: Handbook of Practical Logic and Automated Reasoning · 2009
Later among the works it cites.
In: E. Clarke, A. Voronkov (eds.) Proceedings of the 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning, no. 6355 in Lecture Notes in Artificial Intelligence, pp. 1–12. Springer-Verlag (2010)
Sutcliffe, G.: The TPTP World - Infrastructure for Automated Reasoning · 2010
Later among the works it cites.
Annals of Mathematics and Artificial Intelligence 61
Bundy, A.: Automated theorem provers: a practical tool for the working mathematician? · 2011
Later among the works it cites.
Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R., Biha, S.O., et al.: A machine-checked proof of the odd order theorem (2013)
2013
Closest in time.