Automated Theorem Proving

The goal of Automated Theorem Proving is to automatically generate proofs in a formal language given a conjecture (target theorem) and a knowledge base of known facts. This technology has significant application value in many fields, including the verification and synthesis of software and hardware systems.