Paper Info
Title
Superposition As A Logical Glue
Abstract
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. Superposition provides the key ingredient for a "smart" application tactic that allows the user to disregard many tedious details otherwise needed to convince the system that his reasoning step is indeed correct. We also show how this kind of automation, named small scale, can serve as the building block for the more general, large scale, case, allowing a smooth integration of equational reasoning with backward-based proof searching procedures.
Year
DOI
Venue
2009
10.4204/EPTCS.53.1
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Field
DocType
Issue
Notation,Superposition principle,Programming language,Computer science,Exploit,Automation,Isomorphism,Superposition calculus,Artificial intelligence,Language of mathematics,Gas meter prover
Journal
53
ISSN
Citations 
PageRank 
2075-2180
2
0.40
References 
Authors
14
2
Name
Order
Citations
PageRank
Andrea Asperti184975.19
Enrico Tassi232721.79