34 views

Skip to first unread message

Jan 20, 2024, 3:01:32 PMJan 20

to leo-editor

Here is the link.

I was able to access the paper without a subscription. The solution is left as an exercise for the reader.

We haven't seen anything yet :-)

Edward

Jan 20, 2024, 3:14:05 PMJan 20

to leo-editor

On Saturday, January 20, 2024 at 2:01:32 PM UTC-6 Edward K. Ream wrote:

Here is the link.

From Figure 3:

a, We first sample a large set of random theorem premises.

b, We use the symbolic deduction engine to obtain a deduction closure.

For each node in the graph, we perform traceback to find its minimal set of necessary premise and dependency deductions.

Edward

Jan 20, 2024, 3:21:23 PMJan 20

to leo-editor

On Saturday, January 20, 2024 at 2:14:05 PM UTC-6 Edward K. Ream wrote:

From Figure 3:a, We first sample a large set of random theorem premises.b, We use the symbolic deduction engine to obtain a deduction closure.This returns a directed acyclic graph of statements.

I read the caption before the introduction, which provides better context:

QQQ

Next we use a symbolic deduction engine on the sampled premises.

The engine quickly deduces new true statements by following forward inference rules as shown in Fig. 3b. This returns a directed acyclic graph of all reachable conclusions.

Each node in the directed acyclic graph is a reachable conclusion, with edges connecting to its

parent nodes thanks to the traceback algorithm described in Methods. This allows a traceback process to run recursively starting from any node N, at the end returning its dependency subgraph G(N), with its

root being N and its leaves being a subset of the sampled premises.

parent nodes thanks to the traceback algorithm described in Methods. This allows a traceback process to run recursively starting from any node N, at the end returning its dependency subgraph G(N), with its

root being N and its leaves being a subset of the sampled premises.

Denoting this subset as P, we obtained a synthetic training example

(premises, conclusion, proof) = (P, N, G(N)).

QQQ

Edward

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu