Abstract
This paper presents a principle for using locations in logical expressions to guide the process of building proofs. Using a sequent style presentation of theorem provers, we annotate the inference rules to specify an algorithm that associates the construction of a proof tree to a location within a goal sequent. This principle provides a natural and effective use of the mouse in the user-interface of computer proof assistants. The implementation of the algorithm in a variety of theorem provers is discussed.
Cite
CITATION STYLE
Bertot, Y., Kahn, G., & Théry, L. (1994). Proof by pointing. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 789 LNCS, pp. 141–160). Springer Verlag. https://doi.org/10.1007/3-540-57887-0_94
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
