技术摘要：
本实施例公开了一种定理检索方法、装置、设备及存储介质，涉及云计算领域。该方法包括：获取用户当前输入的定理类型检索信息，根据所述定理类型检索信息，获取所述定理类型检索信息对应的定理类型集合，向所述用户展示所述定理类型集合，以使所述用户确定所需的定理类  全部
背景技术：
随着计算机技术的不断发展，计算机可实现的功能应用也越来越多，给人们带来 了极大的方便。 目前，为了降低人们推理或证明数学定理的工作量，通常使用计算机来自动地进 行推理或证明形式化的数学定理，也就是，将数学定理表达为编程语言中的定理类型，通过 引用辅助定理类型或引理类型来自动地推理或证明数学定理。 在实际应用中，由于引用辅助定理类型或引理类型时需要显示地去应用，也就是 需要知道所引用的辅助定理类型的名称或引理类型的名称，因此，需要通过定理证明器去 检索已经被证明的辅助定理类型的名称或引理类型的名称。 现有技术中，主要是需要输入完整的辅助定理类型或引理类型来检索辅助定理类 型的名称或引理类型的名称。 但是，在现有技术中，会出现用户没有清晰记得完整的辅助定理类型或引理类型 的情况，这样用户在检索的时候会浪费大量的时间构建检索词，并且如果没有构建到合适 的检索词，也不会搜索到想要的辅助定理类型或引理类型的名称，从而造成检索效率较低。
技术实现要素：
本公开的实施例的一个目的是提供一种定理检索的新技术方案。 根据本公开的实施例的第一方面，提供了一种定理检索方法，包括： 获取用户当前输入的定理类型检索信息； 根据所述定理类型检索信息，获取所述定理类型检索信息对应的定理类型集合； 向所述用户展示所述定理类型集合，以使所述用户确定所需的定理类型。 可选的，其中，获取用户当前输入的定理类型检索信息，包括： 在输入操作完成之前，获取所述用户当前输入的定理类型检索信息。 可选的，其中，在获取用户当前输入的定理类型检索信息之前，所述方法还包括： 判断用户的输入操作满足预设条件。 可选的，其中，所述预设的条件包括：所述用户当前停止输入的时间间隔超过预设 的时间阈值；或所述预设的条件包括：所述用户当前输入的定理类型检索信息超过预设的 长度阈值。 可选的，其中，根据所述定理类型检索信息，获取所述定理类型检索信息对应的定 理类型集合，包括： 判断所述定理类型检索信息是否合法； 若是，则根据所述定理类型检索信息，从后端服务器内获取所述定理类型检索信 4 CN 111597393 A 说　明　书 2/10 页 息对应的定理类型集合。 可选的，其中，所述方法还包括： 若否，则根据所述定理类型检索信息，从本地缓存内获取所述定理类型检索信息 对应的定理类型集合。 可选的，其中，判断所述定理类型检索信息是否合法，包括： 通过抽象语法树算法，将所述定理类型检索信息转化成树结构化的定理类型检索 信息； 根据所述树结构化的定理类型检索信息和预设的语法结构，判断所述定理类型检 索信息是否合法。 可选的，其中，根据所述定理类型检索信息，从后端服务器内获取所述定理类型检 索信息对应的定理类型集合，包括： 将所述定理类型检索信息发送给后端服务器，使所述后端服务器对所述定理类型 检索信息进行分词处理，根据分词后的定理类型检索信息，确定定理类型检索关键词，根据 所述定理类型检索关键词，确定所述定理类型检索信息对应的定理类型集合； 获取所述后端服务器发送的所述定理类型检索信息对应的定理类型集合。 可选的，其中，在向所述用户展示所述定理类型集合之前，所述方法还包括： 从所获取的定理类型集合内选取指定数量的定理类型； 根据所选取的定理类型，重新组建定理类型集合。 根据本公开的实施例的第二方面，提供了一种定理检索装置，包括： 第一获取模块，用于获取用户当前输入的定理类型检索信息； 第二获取模块，用于根据所述定理类型检索信息，获取所述定理类型检索信息对 应的定理类型集合； 展示模块，用于向所述用户展示所述定理类型集合，以使所述用户确定所需的定 理类型。 根据本公开的实施例的第三方面，提供了一种定理检索设备，包括定理检索装置； 或者， 所述设备包括：处理器和存储器； 所述存储器用于存储可执行的指令，所述指令用于控制所述处理器执行根据第一 方面中任一项所述的方法。 根据本公开的实施例的第四方面，提供了一种计算机存储介质，所述存储介质存 储有计算机指令，当所述存储介质中的计算机指令由处理器执行时，实现如第一方面任一 项所述的方法。 在本实施例中，每当用户开始输入定理类型检索信息时，就会进行定理检索，再将 检索的定理类型集合反馈给用户，使用户直接根据反馈的定理类型集合及时调整所输入的 定理类型，无需浪费大量的时间构建检索词，有效的节省了定理检索时间，提高检索效率。 通过以下参照附图对本发明的示例性实施例的详细描述，本发明的其它特征及其 优点将会变得清楚。 5 CN 111597393 A 说　明　书 3/10 页 附图说明 被结合在说明书中并构成说明书的一部分的附图示出了本公开的实施例，并且连 同其说明一起用于解释本公开的实施例的原理。 图1是本公开的实施例提供的一种定理检索设备的硬件配置的框图； 图2是本公开的实施例提供的一种定理检索方法的流程图； 图3是本公开的实施例提供的一种定理检索装置的结构示意图； 图4是本公开的实施例提供的另一种定理检索装置的结构示意图； 图5是本公开的实施例提供的一种定理检索设备的结构示意图。