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 {em smart application} tactic, supporting smart matching between a goal and a given result.
Smart Matching / A.Asperti; E.Tassi. - STAMPA. - 6167:(2010), pp. 263-277. (Intervento presentato al convegno 9th International Conference, MKM 2010 tenutosi a Paris, France nel July 5-10, 2010) [10.1007/978-3-642-14128-7_23].
Smart Matching
ASPERTI, ANDREA;
2010
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 {em smart application} tactic, supporting smart matching between a goal and a given result.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
