Talking with the Theorem Prover to Interactively Solve Natural Language Inference. - Atsushi Sumita; Yusuke Miyao; Koji Mineshima (PACLIC, 2021)