Abstract
The problem of automated theorem finding is one of 33 basic research problems in automated reasoning which was originally proposed by Wos. The problem is still an open problem until now. To solve the problem, a systematic methodology with forward reasoning based on strong relevant logic has been proposed. This paper presents a case study of automated theorem finding in graph theory to show the generality of the methodology, and presents a future direction for automated theorem finding based on the methodology.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Cheng, J.: A Relevant Logic Approach to Automated Theorem Finding. In: The Workshop on Automated Theorem Proving attached to International Symposium on Fifth Generation Computer Systems, pp. 8–15 (1994)
Cheng, J.: Entailment Calculus as the Logical Basis of Automated Theorem Finding in Scientific Discovery. In: Systematic Methods of Scientific Discovery: Papers from the 1995 Spring Symposium, pp. 105–110. AAAI Press - American Association for Artificial Intelligence (1995)
Cheng, J.: A Strong Relevant Logic Model of Epistemic Processes in Scientific Discovery. In: Information Modelling and Knowledge Bases XI. Frontiers in Artificial Intelligence and Applications, pp. 136–159. IOS Press (2000)
Cheng, J.: A Semilattice Model for the Theory Grid. In: Proc. 3rd International Conference on Semantics, Knowledge and Grid, pp. 152–157. IEEE Computer Society (2007)
Cheng, J., Nara, S., Goto, Y.: FreeEnCal: A Forward Reasoning Engine with General-Purpose. In: Apolloni, B., Howlett, R.J., Jain, L. (eds.) KES 2007, Part II. LNCS (LNAI), vol. 4693, pp. 444–452. Springer, Heidelberg (2007)
Colton, S., Meier, A., Sorge, V., McCasland, R.: Automatic Generation of Classification Theorems for Finite Algebras. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 400–414. Springer, Heidelberg (2004)
Diestel, R.: Graph Theory. Springer, Heidelberg (2000)
Gao, H., Goto, Y., Cheng, J.: A Systematic Methodology for Automated Theorem Finding. Theoretical Computer Science 554, 2–21 (2014)
Gao, H., Goto, Y., Cheng, J.: Research on Automated Theorem Finding: Current State and Future Directions. In: Park, J.J(J.H.), Pan, Y., Kim, C.-S., Yang, Y. (eds.) Future Information Technology. LNEE, vol. 309, pp. 105–110. Springer, Heidelberg (2014)
McCasland, R., Bundy, A., Autexier, S.: Automated Discovery of Inductive Theorems. Journal of Studies in Logic, Grammar and Rhetoric 10(23), 135–149 (2007)
Quaife, A.: Automated Development of Fundamental Mathematical Theories. Kluwer Academic (1992)
Recio, T., Velez, M.Z.: Automatic Discovery of Theorems in Elementary Geometry. Journal of Automated Reasoning 23(1), 63–82 (1999)
Tang, P., Lin, F.: Discovering Theorems in Game Theory: Two-Person Games with Unique Pure Nash Equilibrium Payoffs. Artificial Intelligence 175(14), 2010–2020 (2011)
Wos, L.: Automated Reasoning: 33 Basic Research Problem. Prentic-Hall (1988)
Wos, L.: The Problem of Automated Theorem Finding. Journal of Automated Reasoning 10(1), 137–138 (1993)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gao, H., Goto, Y., Cheng, J. (2015). Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic: A Case Study in Graph Theory. In: Park, J., Chao, HC., Arabnia, H., Yen, N. (eds) Advanced Multimedia and Ubiquitous Engineering. Lecture Notes in Electrical Engineering, vol 352. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-47487-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-662-47487-7_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-47486-0
Online ISBN: 978-3-662-47487-7
eBook Packages: EngineeringEngineering (R0)