A formal approach to visual proving based on logic programming
Masami Hagiya · 2003
Gives a general framework for visual proving based on logic programming, by giving a mapping from figures to formulas. For a figure consisting of graphic objects and constraints, the author formally defines the set of facts that are visible in the figure. As a result, one can rigorously formalize the soundness of reasoning by figures.>