自动推理是指使用计算机程序或算法，基于已有的逻辑规则和知识，自动地从已知事实或假设中推导出新的结论或信息的过程。我们主要研究自动推理方向中的命题逻辑求解器及一阶逻辑定理证明器。

命题逻辑求解器是一种计算机程序，用于解决命题逻辑的问题，即只涉及命题（语句的真假）和逻辑运算（如与、或、非等）的推理问题。命题逻辑求解器可以接受命题逻辑的公式作为输入，然后使用一系列逻辑规则和推理方法来自动推导出结论，从而验证输入公式的真假性或者找到可行的解决方案。应用场景包括：自然语言处理、知识表示与推理、人工智能、计算机科学等。

一阶逻辑定理证明器是一种计算机程序，用于验证一阶逻辑公式的真假性，并能够自动证明某些命题是否成立。一阶逻辑是比命题逻辑更为强大和广泛应用的一种逻辑体系，它涉及到量词、谓词、函数、集合等概念，可以描述更为复杂的逻辑结构。一阶逻辑定理证明器可以接受一阶逻辑公式作为输入，然后使用一系列的证明策略和规则来自动推导出一个证明，从而验证输入公式的真假性或者证明某个命题的正确性。应用场景包括：软件验证、硬件验证、自动化推理、形式化证明等。