Previous research has explored criteria for evaluating the simplicity and readability of geometric proofs generated by theorem provers, primarily from a human perspective. In particular, Graziani and Quaresma examined the simplicity and readability of proofs produced by theorem provers implementing the area method, introducing geometrographic coefficients to quantify different aspects of proof complexity. Building on their work, this study extends their analysis by investigating the computational effort involved in the proof process, specifically by measuring CPU time. The objective is to determine whether, within the context of proof generation, the hypothesised human effort aligns with the machine’s measured computational workload. Given the strong connection between human effort and proof readability, this comparison may offer valuable insights for improving the readability of machine-generated proofs by considering both human cognitive constraints and computational limitations.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Towards a Readability Criterion for Humans and Machines

  • Pedro Quaresma,
  • Pierluigi Graziani

摘要

Previous research has explored criteria for evaluating the simplicity and readability of geometric proofs generated by theorem provers, primarily from a human perspective. In particular, Graziani and Quaresma examined the simplicity and readability of proofs produced by theorem provers implementing the area method, introducing geometrographic coefficients to quantify different aspects of proof complexity. Building on their work, this study extends their analysis by investigating the computational effort involved in the proof process, specifically by measuring CPU time. The objective is to determine whether, within the context of proof generation, the hypothesised human effort aligns with the machine’s measured computational workload. Given the strong connection between human effort and proof readability, this comparison may offer valuable insights for improving the readability of machine-generated proofs by considering both human cognitive constraints and computational limitations.