2 papers
cs.CL2025
Natural Language Translation of Formal Proofs through Informalization of Proof Steps and Recursive Summarization along Proof Structure
Seiji Hattori, Takuya Matsuzaki, Makoto Fujiwara
This paper proposes a natural language translation method for machine-verifiable formal proofs that leverages the informalization (verbalization of formal language proof steps) and…
math.LO2025
Hierarchical formula classes with respect to semi-classical prenex normalization
Makoto Fujiwara, Taishi Kurahashi
In [10], the authors formalized the standard transformation procedure for prenex normalization of first-order formulas and showed that the classes and …