TL;DR
This paper introduces a superposition-based smart matching feature in the Matita theorem prover, enabling automatic transformations akin to human mathematical reasoning for improved proof automation.
Contribution
It presents the implementation of a smart application tactic that performs smart matching, enhancing the flexibility and automation in interactive theorem proving.
Findings
Implemented smart matching in Matita using superposition
Improved proof automation with smart application tactic
Facilitated implicit transformations in formal proofs
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 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMathematics, Computing, and Information Processing · Advanced Database Systems and Queries · Semantic Web and Ontologies