Abstract
After setting a context based on two general points (that humans appear to reason in infinitary fashion, and two, that actual hypercomputers aren’t currently available to directly model and replicate such infinitary reasoning), we set a humble engineering goal of taking initial steps toward a computing machine that can reason in infinitary fashion. The initial steps consist in our outline of automated proof-verification and proof-discovery techniques for theorems independent of PA that seem to require an understanding and use of infinitary concepts (e.g., Goodstein’s Theorem). We specifically focus on proof-discovery techniques that make use of a marriage of analogical and deductive reasoning (which we call analogico-deductive reasoning).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arkoudas, K., Bringsjord, S.: Metareasoning for Multi-agent Epistemic Logics. In: Leite, J., Torroni, P. (eds.) CLIMA 2004. LNCS (LNAI), vol. 3487, pp. 111–125. Springer, Heidelberg (2005), http://kryten.mm.rpi.edu/arkoudas.bringsjord.clima.crc.pdf
Baker, S., Ireland, A., Smaill, A.: On the Use of the Constructive Omega-Rule Within Automated Deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 214–225. Springer, Heidelberg (1992)
Bringsjord, S., Arkoudas, K.: On the Provability, Veracity, and AI-Relevance of the Church-Turing Thesis. In: Olszewski, A., Wolenski, J., Janusz, R. (eds.) Church’s Thesis After 70 Years, pp. 66–118. Ontos Verlag, Frankfurt (2006), http://kryten.mm.rpi.edu/ct_bringsjord_arkoudas_final.pdf ; This book is in the series Mathematical Logic, edited by W. Pohlers, T. Scanlon, E. Schimmerling, R. Schindler, H. Schwichtenberg
Bringsjord, S., Govindarajulu, N.S.: In Defense of the Unprovability of the Church-Turing Thesis. Journal of Unconventional Computing 6, 353–373 (2011); Preprint available at http://kryten.mm.rpi.edu/SB_NSG_CTTnotprovable_091510.pdf
Bringsjord, S., Licato, J.: Psychometric Artificial General Intelligence: The Piaget-MacGyver Room. In: Wang, P., Goertzel, B. (eds.) Theoretical Foundations of Artificial General Intelligence. Atlantis Press (2012), http://kryten.mm.rpi.edu/Bringsjord_Licato_PAGI_071512.pdf
Bringsjord, S., Taylor, J., Shilliday, A., Clark, M., Arkoudas, K.: Slate: An Argument-Centered Intelligent Assistant to Human Reasoners. In: Grasso, F., Green, N., Kibble, R., Reed, C. (eds.) Proceedings of the 8th International Workshop on Computational Models of Natural Argument, CMNA 2008, Patras, Greece, pp. 1–10 (2008), http://kryten.mm.rpi.edu/Bringsjord_etal_Slate_cmna_crc_061708.pdf
Bringsjord, S., van Heuveln, B.: The Mental Eye Defense of an Infinitized Version of Yablo’s Paradox. Analysis 63(1), 61–70 (2003)
Bringsjord, S., Zenzen, M.: Superminds: People Harness Hypercomputation, and More. Kluwer Academic Publishers, Dordrecht (2003)
Ebbinghaus, H.D., Flum, J., Thomas, W.: Mathematical Logic. Springer, New York (1984)
Franzén, T.: Transfinite Progressions: A Second Look at Completeness. Bulletin of Symbolic Logic, 367–389 (2004)
Kolmogorov, A., Uspenskii, V.: On the Definition of an Algorithm. Uspekhi Matematicheskikh Nauk 13(4), 3–28 (1958)
Licato, J., Bringsjord, S., Hummel, J.E.: Exploring the Role of Analogico-Deductive Reasoning in the Balance-Beam Task. In: Rethinking Cognitive Development: Proceedings of the 42nd Annual Meeting of the Jean Piaget Society, Toronto, Canada (2012), https://docs.google.com/open?id=0B1S661sacQp6NDJ0YzVXajJMWVU
Licato, J., Govindarajulu, N.S., Bringsjord, S., Pomeranz, M., Gittelson, L.: Analogico-deductive Generation of Gödel’s First Incompleteness Theorem from the Liar Paradox. In: Proceedings of the 23rd Annual International Joint Conference on Artificial Intelligence, IJCAI 2013 (2013)
Owen, S.: Analogy for Automated Reasoning. Academic Press (1990)
Pelletier, J.: A Brief History of Natural Deduction. History and Philosophy of Logic 20, 1–31 (1999)
Polya, G.: Induction and Analogy in Mathematics. Princeton University Press, Princeton (1954); This is Volume I of Mathematics and Plausible Reasoning. Volume II is Patterns of Plausible Inference
Potter, M.: Set Theory and its Philosophy: A Critical Introduction. Oxford University Press, Oxford (2004)
Robinson, J.: A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM (JACM) 12(1), 23–41 (1965)
Shilliday, A.: Elisa: A New System for AI-assisted Logico-mathematical Scientific Discovery Incorporating Novel Techniques in Infinite Model Finding. PhD thesis, Rensselaer Polytechnic Institute (2009)
Smith, P.: An Introduction to Gödel’s Theorems. Cambridge University Press, Cambridge (2007)
Stickel, M.E.: SNARK: SRI’s New Automated Reasoning Kit SNARK (2008), http://www.ai.sri.com/~stickel/snark.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Govindarajulu, N.S., Licato, J., Bringsjord, S. (2013). Small Steps toward Hypercomputation via Infinitary Machine Proof Verification and Proof Generation. In: Mauri, G., Dennunzio, A., Manzoni, L., Porreca, A.E. (eds) Unconventional Computation and Natural Computation. UCNC 2013. Lecture Notes in Computer Science, vol 7956. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39074-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-39074-6_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39073-9
Online ISBN: 978-3-642-39074-6
eBook Packages: Computer ScienceComputer Science (R0)