Utilizing the High-Level Nature

• Hypothesis: Formal tactic-style proof steps closely approximate human proof steps.

  • A one-to-one mapping of proof nodes to sentences can be used

• Evidence: study of human performance on generation task

Type of mapping

# occurrences

% occurrences

1-1

180

64%

1-2

52

19%

1-3

12

4%

2-1

23

8%

3-1, 4-1

8

3%

1-0

4

1%

0-1

1

ə%

1-1, 1-2, 2-1

255

91%

1-1, case split or analogy

232

83%

Previous slide

Next slide

Back to first slide

View graphic version