International Business Machines Corporation

Maxwell Crouse

Achille Belly Fokoue-Nkoutche

Kavitha Srinivas

Lingfei Wu

Maria Chang

Ibrahim Abdelaziz

Michael John Witbrock

Ryan A Musa

Cristina Cornelio

Bassem Makni

Veronika Thost

Generate, from a logical formula, a directed acyclic graph having a plurality of nodes and a plurality of edges. Assign an initial embedding to each mode and edge, to one of a plurality of layers. Compute a plurality of initial node states by using feed-forward networks, and construct cross-dependent embeddings between conjecture node embeddings and premise node embeddings. Topologically sort the DAG with the initial embeddings and node states. Beginning from a lowest rank, compute layer-by-layer embedding updates for each of the plurality of layers until a root is reached. Assign the embedding update for the root node as a final embedding for the DAG. Provide the final embedding for the DAG as input to a machine learning system, and carry out the automatic theorem proving with same.

Capturing the global structure of logical formulae with graph long short-term memory

Systems, computer-implemented methods, and computer program products that can facilitate encoding a tree data structure into a vector based on a set of constraints are provided. According to an embodiment, a system can comprise a memory that stores computer executable components and a processor that executes the computer executable components stored in the memory. The computer executable components can comprise a constraint former that can form a set of constraints based on a first tree data structure and a vector encoder that can encode the first tree data structure into a vector based on the set of constraints.

Encoding and decoding tree data structures as vector data structures

Growing community of inventors

Chicago, IL, United States of America

Maxwell Crouse