Computer Science – Logic in Computer Science
Scientific paper
2010-05-03
Computer Science
Logic in Computer Science
To appear in The 9th International Conference on Mathematical Knowledge Management: MKM 2010
Scientific paper
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 behavior 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.
Asperti Andrea
Tassi Enrico
No associations
LandOfFree
Smart matching does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Smart matching, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Smart matching will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-659021