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