### Can we do ATP without accumulative lemmas?

Can we do ATP without accumulative lemmas?

#### Cut elimination

Cut elimination

## [Structure]

[Structure]

### There are paths that correspond to proofs [ expression -> expression ]

There are paths that correspond to proofs [ expression -> expression ]

### For [ statement -> statement ] the proof is a tree

For [ statement -> statement ] the proof is a tree

could be past entailment cone of what is being proved .... but instead, want to find a tautology in the intersection of future entailment cones

### One can find these paths in entailment cones

One can find these paths in entailment cones

can be untangled by cut elimination to a straight line path

#### Can we make a non-accumulative proof?

Can we make a non-accumulative proof?

## Finding Nontrivial ATP Proofs

Finding Nontrivial ATP Proofs

In[]:=

axlist=SortBy[Union[First[Sort[{#,#/.{a->b,b->a}}]]&/@DeleteCases[Union[Sort/@canonicalizePatterns/@(TwoWayRule@@@Tuples[(Flatten[Groupings[#,SmallCircle->2]&/@Table[Tuples[{a,b},n],{n,3}]]/.{a->a_,b->b_}),2])]/.{p_Pattern:>First[p],TwoWayRule->Equal},Except[_Equal]]],StringLength[ToString[#]]&]

Out[]=

In[]:=

Clear[a]

In[]:=

ParallelEvaluate[Clear[a]]

Out[]=

{Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null,Null}

In[]:=

ParallelMap[#->FindEquationalProof[#,ForAll[{a,b},a==a∘b],"ProofGraph",TimeConstraint4]&,%249]

In[]:=

ProofObjectToTokenEventGraph[FindEquationalProof[(a∘a)∘a(a∘b)∘b,ForAll[{a,b},a==a∘b]]]

Out[]=

x∘y==(y∘x)∘y

In[]:=

ParallelMap[#->FindEquationalProof[#,ForAll[{a,b},a==a∘(a∘b)],"ProofGraph",TimeConstraint4]&,%249]

Out[]=

In[]:=

ProofObjectToTokenEventGraph[FindEquationalProof[a(a∘a)∘a,ForAll[{a,b},a==a∘(a∘b)]]]

Out[]=

a(a∘a)∘a

In[]:=

DeleteCases[ParallelMap[#->FindEquationalProof[#,ForAll[{a,b},a==a∘(a∘b)],TimeConstraint4]&,Union[Sort/@(First[Sort[{#,#/.{a->b,b->a}}]]&/@DeleteCases[Equal@@@Tuples[Flatten[Groupings[#,SmallCircle->2]&/@Catenate[Table[Tuples[{a,b},n],{n,4}]]],2],True])]],_->_Failure]

In[]:=

TakeLargestBy[%267,#[[2]]["ProofLength"]&,10]

Out[]=

(a∘a)∘(a∘b)((a∘a)∘a)∘aProofObject,a∘((a∘a)∘b)((a∘a)∘a)∘aProofObject,a∘((a∘a)∘a)a∘((a∘a)∘b)ProofObject,a∘((a∘a)∘a)((a∘a)∘a)∘aProofObject,a∘((a∘a)∘a)(a∘(a∘b))∘aProofObject,a∘((a∘a)∘a)(a∘a)∘(a∘b)ProofObject,a∘(a∘(b∘a))((a∘a)∘a)∘aProofObject,a∘((a∘a)∘b)(a∘a)∘aProofObject,a∘(a∘b)((a∘a)∘a)∘aProofObject,a∘(a∘(b∘b))((a∘a)∘a)∘aProofObject

## Looking for good critical pair lemmas

Looking for good critical pair lemmas

Proves a complicated tautology

#### Remote Batch Job

Remote Batch Job

### Additional Cases

Additional Cases

## Confluent rewriting

Confluent rewriting