Abstract
One of the most annoying aspects in the formalization of mathematics is the need of transforming notions to match a given, existing result. This kind of transformations, often based on a conspicuous background knowledge in the given scientific domain (mostly expressed in the form of equalities or isomorphisms), are usually implicit in the mathematical discourse, and it would be highly desirable to obtain a similar behaviour in interactive provers. The paper describes the superposition-based implementation of this feature inside the Matita interactive theorem prover, focusing in particular on the so called smart application tactic, supporting smart matching between a goal and a given result.
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
Ahrendt, W., Beckert, B., Hähnle, R., Menzel, W., Reif, W., Schellhorn, G., Schmitt, P.H.: Integrating automated and interactive theorem proving. In: Automated Deduction — A Basis for Applications. Systems and Implementation Techniques of Applied Logic Series, vol. II(9), pp. 97–116. Kluwer, Dordrecht (1998)
Armando, A., Ranise, S., Rusinowitch, M.: Uniform derivation of decision procedures by superposition. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 513–527. Springer, Heidelberg (2001)
Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: Hints in unification. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol. 5674, pp. 84–98. Springer, Heidelberg (2009)
Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: A compact kernel for the Calculus of Inductive Constructions. Sadhana 34(1), 71–144 (2009)
Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. Journal of Automated Reasoning 39(2), 109–139 (2007)
Asperti, A., Tassi, E.: Higher order proof reconstruction from paramodulation-based refutations: The unit equality case. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 146–160. Springer, Heidelberg (2007)
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)
Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. J. Autom. Reasoning 29(3-4), 253–275 (2002)
The Coq proof-assistant (2009), http://coq.inria.fr
Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Handbook of Automated Reasoning, pp. 611–706. Elsevier and MIT Press (2001)
Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 279–301 (1982)
Dershowitz, N., Hsiang, J., Josephson, N.A., Plaisted, D.A.: Associative-commutative rewriting. In: IJCAI, pp. 940–944 (1983)
Ganzinger, H., Nieuwenhuis, R., Nivela, P.: Fast term indexing with coded context trees. J. Autom. Reasoning 32(2), 103–120 (2004)
Graf, P.: Substitution tree indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 117–131. Springer, Heidelberg (1995)
Hurd, J.: Integrating gandalf and hol. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 311–322. Springer, Heidelberg (1999)
Hurd, J.: First-order proof tactics in higher-order logic theorem provers. Technical Report NASA/CP-2003-212448, Nasa technical reports (2003)
Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational problems in Abstract Algebra, pp. 263–297 (1970)
McCune, W.: Experiments with discrimination tree indexing and path indexing for term retrieval. Journal of Automated Reasoning 9(2), 147–167 (1992)
Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning 40(1), 35–60 (2008)
Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: First prototype. Inf. Comput. 204(10), 1575–1596 (2006)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based thorem proving. In: Handbook of Automated Reasoning, pp. 443–471. Elsevier/MIT Press (2001)
Paulson, L.C.: A generic tableau prover and its integration with isabelle. J. UCS 5(3), 73–87 (1999)
Riazanov, A., Voronkov, A.: The design and implementation of vampire. AI Communications 15(2-3), 91–110 (2002)
Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. J. Symb. Comput. 36(1-2), 101–115 (2003)
Sacerdoti Coen, C., Tassi, E.: A constructive and formal proof of Lebesgue’s dominated convergence theorem in the interactive theorem prover Matita. Journal of Formalized Reasoning 1, 51–89 (2008)
Sozeau, M.: A new look at generalized rewriting in type theory. Journal of Formalized Reasoning 2(1), 41–62 (2009)
Sutcliffe, G.: The 4th ijcar automated theorem proving system competition - casc-j4. AI Commun. 22(1), 59–72 (2009)
Wos, L., Robinson, G.A., Carson, D.F., Shalla, L.: The concept of demodulation in theorem proving. J. ACM 14(4), 698–709 (1967)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Asperti, A., Tassi, E. (2010). Smart Matching. In: Autexier, S., et al. Intelligent Computer Mathematics. CICM 2010. Lecture Notes in Computer Science(), vol 6167. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14128-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-14128-7_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14127-0
Online ISBN: 978-3-642-14128-7
eBook Packages: Computer ScienceComputer Science (R0)