上江洲の述語論理に
自然言語→証明体系（NJ）の
仮定が詳述されてる。