Notice of Pre-AIA or AIA Status
The present application, filed on or after March 16, 2013, is being examined under the first inventor to file provisions of the AIA .
DETAILED ACTION
Claims 1-20 are pending in this office action.
Information Disclosure Statement
The information disclosure statements (IDS) submitted on July 14, 2023, and September 15, 2023, are in compliance with the provisions of 37 CFR 1.97. Accordingly, the information disclosure statement is being considered by the examiner.
Claim Rejections - 35 USC § 103
The following is a quotation of 35 U.S.C. 103 which forms the basis for all obviousness rejections set forth in this Office action:
A patent for a claimed invention may not be obtained, notwithstanding that the claimed invention is not identically disclosed as set forth in section 102, if the differences between the claimed invention and the prior art are such that the claimed invention as a whole would have been obvious before the effective filing date of the claimed invention to a person having ordinary skill in the art to which the claimed invention pertains. Patentability shall not be negated by the manner in which the invention was made.
Claims 1-20 are rejected under 35 U.S.C. 103 as being unpatentable over Saxe et al. (U.S. Patent No. 6,343,376) in view of Wang et al. (Premise Selection for Theorem Proving by Deep Graph Embedding, 2017).
Regarding claims 1, 8, and 15, Saxe et al. teaches a system, comprising: a processor that executes computer-executable components stored in a non-transitory computer-readable memory, the computer-executable components comprising (col. 5, line 64 through col. 6, line 5): an access component that accesses a set of first directed acyclic graphs respectively representing a conjecture and a set of axioms (col. 1, lines 18-32 and col. 6, lines 45-52); and based on a second directed acyclic graph that is an aggregation of the set of first directed acyclic graphs (col. 7, line 62 through col. 8, line 5, e-graph maintains equivalence classes by merging nodes which aggregates the set of individual logical formulas into a single unified representation).
Saxe et al. does not teach a proof component that generates, via execution of at least one neural-guided automated theorem prover that independently processes the set of first directed acyclic graphs, a proof for the conjecture, wherein the at least one neural-guided automated theorem prover leverages, for a node representing a non-logical symbol name present in more than one of the set of first directed acyclic graphs, a name-invariant learned embedding.
Wang et al. teaches a proof component that generates, via execution of at least one neural-guided automated theorem prover that independently processes the set of first directed acyclic graphs, a proof for the conjecture, wherein the at least one neural-guided automated theorem prover leverages, for a node representing a non-logical symbol name present in more than one of the set of first directed acyclic graphs, a name-invariant learned embedding (section 1, paragraph 6 and 10).
It would have been obvious to one of ordinary skill in the art, before the effective filing date of the claimed invention, to combine a neural-guided prover for representing non-logical symbol names by a name-invariant learned embedding, as taught by Wang et al., with the method of Saxe et al. It would have been obvious for such modifications because reliability is increased when name-invariant graphs are used to prevent issues with misnamed variables (see section 1, paragraph 6 of Wang et al.).
Regarding claims 2, 9, and 16, Saxe et al. teaches wherein the computer-executable components further comprise: an aggregation component that generates the second directed acyclic graph, by combining the set of first directed acyclic graphs via a conjunction, and by collapsing together repeated instances of the node representing the non-logical symbol name (col. 6, lines 45-52 and e-graph maintaining equivalence).
Regarding claims 3, 10, and 17, Saxe et al. as modified by Wang et al. teaches wherein the computer-executable components further comprise: an embedding component that feeds the second directed acyclic graph and random embeddings respectively corresponding to nodes of the second directed acyclic graph as input to a graph neural network, wherein the graph neural network produces as output first learned embeddings respectively corresponding to the nodes of the second directed acyclic graph, and wherein the name-invariant learned embedding is whichever of the first learned embeddings corresponds to the node representing the non-logical symbol name (see section 1, paragraph 7 of Wang et al.).
Regarding claims 4, 11, and 18, Saxe et al. as modified by Wang et al. teaches wherein, during independent processing of any of the set of first directed acyclic graphs in which the node representing the non-logical symbol name is present, the at least one neural-guided automated theorem prover uses, as an initial embedding for the node representing the non-logical symbol name, the name-invariant learned embedding instead of a random embedding (see section 4.6, paragraph 2 of Wang et al.).
Regarding claims 5, 12, and 19, Saxe et al. as modified by Wang et al. teaches wherein the at least one neural-guided automated theorem prover comprises an ensemble of neural-guided automated theorem provers, each of which is set to a distinct proof configuration (see section 2, paragraph 1 of Wang et al.).
Regarding claims 6, 13, and 20, Saxe et al. teaches wherein the non-logical symbol name is a name of a constant, of a function, or of a predicate that is present in the conjecture or in the set of axioms (col. 2, lines 17-24).
Regarding claims 7 and 14, Saxe et al. teaches wherein the computer-executable components comprise: a result component that visually renders the proof on an electronic display (col. 6, lines 61-67).
Any inquiry concerning this communication or earlier communications from the examiner should be directed to BRANDON HOFFMAN whose telephone number is (571)272-3863. The examiner can normally be reached Monday-Friday 8:30AM-5:00PM.
Examiner interviews are available via telephone, in-person, and video conferencing using a USPTO supplied web-based collaboration tool. To schedule an interview, applicant is encouraged to use the USPTO Automated Interview Request (AIR) at http://www.uspto.gov/interviewpractice.
If attempts to reach the examiner by telephone are unsuccessful, the examiner’s supervisor, Jeffrey Pwu can be reached at (571)272-6798. The fax phone number for the organization where this application or proceeding is assigned is 571-273-8300.
Information regarding the status of published or unpublished applications may be obtained from Patent Center. Unpublished application information in Patent Center is available to registered users. To file and manage patent submissions in Patent Center, visit: https://patentcenter.uspto.gov. Visit https://www.uspto.gov/patents/apply/patent-center for more information about Patent Center and https://www.uspto.gov/patents/docx for information about filing in DOCX format. For additional questions, contact the Electronic Business Center (EBC) at 866-217-9197 (toll-free). If you would like assistance from a USPTO Customer Service Representative, call 800-786-9199 (IN USA OR CANADA) or 571-272-1000.
/BRANDON HOFFMAN/Primary Examiner, Art Unit 2433
Prosecution Insights