Computer Science – Logic in Computer Science
Scientific paper
2011-03-17
EPTCS 53, 2011, pp. 1-15
Computer Science
Logic in Computer Science
In Proceedings TYPES 2009, arXiv:1103.3111
Scientific paper
10.4204/EPTCS.53.1
The typical mathematical language systematically exploits notational and logical abuses whose resolution requires not just the knowledge of domain specific notation and conventions, but not trivial skills in the given mathematical discipline. A large part of this background knowledge is expressed in form of equalities and isomorphisms, allowing mathematicians to freely move between different incarnations of the same entity without even mentioning the transformation. Providing ITP-systems with similar capabilities seems to be a major way to improve their intelligence, and to ease the communication between the user and the machine. The present paper discusses our experience of integration of a superposition calculus within the Matita interactive prover, providing in particular a very flexible, "smart" application tactic, and a simple, innovative approach to automation.
Asperti Andrea
Tassi Enrico
No associations
LandOfFree
Superposition as a logical glue 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 Superposition as a logical glue, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Superposition as a logical glue will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-247369