Abstract
We introduce a fully automatic system, implemented in the Lean theorem prover, that solves equality problems of everyday mathematics. Our overriding priority in devising the system is that it should construct proofs of equality in a way that is similar to that of humans. A second goal is that the methods it uses should be domain independent. The basic strategy of the system is to operate with a subtask stack: whenever there is no clear way of making progress towards the task at the top of the stack, the program finds a promising subtask, such as rewriting a subterm, and places that at the top of the stack instead. Heuristics guide the choice of promising subtasks and the rewriting process. This makes proofs more human-like by breaking the problem into tasks in the way that a human would. We show that our system can prove equality theorems simply, without having to preselect or orient rewrite rules as in standard theorem provers, and without having to invoke heavy duty tools for performing simple 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
References
Baader, F., Nipkow, T.: Term Rewriting and All that. Cambridge University Press, Cambridge (1999)
Blum, A.L., Furst, M.L.: Fast planning through planning graph analysis. Artif. Intell. 90(1–2), 281–300 (1997)
Böhme, S., Nipkow, T.: Sledgehammer: judgement day. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 107–121. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14203-1_9
Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111–120. Springer, Heidelberg (1988). https://doi.org/10.1007/BFb0012826
Bundy, A.: A critique of proof planning. In: Kakas, A.C., Sadri, F. (eds.) Computational Logic: Logic Programming and Beyond. LNCS (LNAI), vol. 2408, pp. 160–177. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45632-5_7
Bundy, A.: Automated theorem provers: a practical tool for the working mathematician? Ann. Math. Artif. Intell. 61(1), 3 (2011). https://doi.org/10.1007/s10472-011-9248-8
Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005). https://doi.org/10.1007/11541868_7
Hoek, K., Morrison, S.: Lean-rewrite-search repository (2019). https://github.com/semorrison/lean-rewrite-search
Kambhampati, S., Knoblock, C.A., Yang, Q.: Planning as refinement search: a unified framework for evaluating design tradeoffs in partial-order planning. Artif. Intell. 76(1), 167–238 (1995)
Langley, P., Choi, D., Trivedi, N.: Icarus user’s manual. Institute for the Study of Learning and Expertise 2164 (2011)
Melis, E., Siekmann, J.: Knowledge-based proof planning. Artif. Intell. 115(1), 65–105 (1999)
de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378–388. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_26
Tate, A.: Generating project networks. In: Proceedings of the 5th International Joint Conference on Artificial Intelligence, vol. 2, pp. 888–893. Morgan Kaufmann Publishers Inc. (1977)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Ayers, E.W., Gowers, W.T., Jamnik, M. (2019). A Human-Oriented Term Rewriting System. In: Benzmüller, C., Stuckenschmidt, H. (eds) KI 2019: Advances in Artificial Intelligence. KI 2019. Lecture Notes in Computer Science(), vol 11793. Springer, Cham. https://doi.org/10.1007/978-3-030-30179-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-30179-8_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30178-1
Online ISBN: 978-3-030-30179-8
eBook Packages: Computer ScienceComputer Science (R0)