Wangd-asr-book

some tips for chapter 1:

Automatic reasoning (proof)

DeepAlgebra - an outline of a program (a NLP frontend that convert natural langauge to formal terms) https://arxiv.org/pdf/1610.01044v1.pdf

Iterative Theorem Provers (ITPs) such as COQ [5] or Mizar[12] [2] (Other standard ITPs include HOL (Light), Isabelle and ACL2.) Automatic Theorem Prover (ATP), for example E [14] [15] (Other standard ATPs include Vampyre, Z3 and JProver.)

COQ: iterative Theorem Provers (ITP) https://coq.inria.fr/about-coq