RTE does not work with the newer version of Coq

[ishowta]

問題点

明らかに含意しているのにrte_ja.shの出力がunknownとなってしまいます。
Coqについて勉強不足で、何が問題なのか分かりませんでした。
ReadmeでCoqのバージョンが指定されておらず、かつ最新のCoq8.11でRTEが動作しません。

環境

• python: 3.7.9
• coq: 8.11.2
• ccg2lambda: master branch (442a9ec)
• OS: WSL Ubuntu20.04

やったこと

1. Readmeに書いてあるセットアップをしました。
2. 日本語のRTEを行うために、emnlp2016exp.shを参考にして以下のセットアップを行いました。

   cp ja/coqlib_ja.v coqlib.v
   coqc coqlib.v
   cp ja/tactics_coq_ja.txt tactics_coq.txt
   

3. sentence.txtに同じ文を入れました。（明らかに含意しているので）

   ソクラテスは人間である。
   ソクラテスは人間である。
   

4. 以下のスクリプトを実行しました。

    ./ja/rte_ja.sh out/sentence.txt ja/semantic_templates_ja_event.yaml 
   

   Output

   unknown
   

調べたこと

• 手動でCoqを動かすとnltac_set; nltac_final.のところでNo such goal.と出て止まりました。

  Require Export coqlib.
  Parameter _ソクラテス : Entity.
  Parameter _人間 : Entity -> Prop.
  Theorem t1: (and True (exists x, (and (_人間 x) (exists e, (and (and ((Nom e) = x) True) ((Nom e) = _ソクラテス)))))) -> (and True (exists x, (and (_人間 x) (exists e, (and (and ((Nom e) = x) True) ((Nom e) = _ソクラテス)))))). Set Firstorder Depth 1. nltac. nltac_set; nltac_final. Set Firstorder Depth 3. nltac_final. Qed.
  

参照

ccg2lambda/scripts/theorem.py

Lines 337 to 343 in 442a9ec

	# Check whether the string "is defined" appears in the output of coq.
	# In that case, we return True. Otherwise, we return False.
	def is_theorem_defined(output_lines):
	for output_line in output_lines:
	if len(output_line) > 2 and 'is defined' in output_line:
	return True
	return False

[ishowta]

I downgraded Coq from 8.11 to 8.3 and it worked fine.