WOLFRAM NOTEBOOK

Can we do ATP without accumulative lemmas?

Cut elimination

[Structure]

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

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

can be untangled by cut elimination to a straight line path

Can we make a non-accumulative proof?

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
Logic: EquationalLogic
Steps: 8
Theorem: (a∘a)∘(a∘b)((a∘a)∘a)∘a
,a∘((a∘a)∘b)((a∘a)∘a)∘aProofObject
Logic: EquationalLogic
Steps: 8
Theorem: a∘((a∘a)∘b)((a∘a)∘a)∘a
,a∘((a∘a)∘a)a∘((a∘a)∘b)ProofObject
Logic: EquationalLogic
Steps: 7
Theorem: a∘((a∘a)∘a)a∘((a∘a)∘b)
,a∘((a∘a)∘a)((a∘a)∘a)∘aProofObject
Logic: EquationalLogic
Steps: 7
Theorem: a∘((a∘a)∘a)((a∘a)∘a)∘a
,a∘((a∘a)∘a)(a∘(a∘b))∘aProofObject
Logic: EquationalLogic
Steps: 7
Theorem: a∘((a∘a)∘a)(a∘(a∘b))∘a
,a∘((a∘a)∘a)(a∘a)∘(a∘b)ProofObject
Logic: EquationalLogic
Steps: 7
Theorem: a∘((a∘a)∘a)(a∘a)∘(a∘b)
,a∘(a∘(b∘a))((a∘a)∘a)∘aProofObject
Logic: EquationalLogic
Steps: 7
Theorem: a∘(a∘(b∘a))((a∘a)∘a)∘a
,a∘((a∘a)∘b)(a∘a)∘aProofObject
Logic: EquationalLogic
Steps: 7
Theorem: a∘((a∘a)∘b)(a∘a)∘a
,a∘(a∘b)((a∘a)∘a)∘aProofObject
Logic: EquationalLogic
Steps: 7
Theorem: a∘(a∘b)((a∘a)∘a)∘a
,a∘(a∘(b∘b))((a∘a)∘a)∘aProofObject
Logic: EquationalLogic
Steps: 7
Theorem: a∘(a∘(b∘b))((a∘a)∘a)∘a

Looking for good critical pair lemmas

Proves a complicated tautology

Remote Batch Job

Additional Cases

Confluent rewriting

Wolfram Cloud

You are using a browser not supported by the Wolfram Cloud

Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.


I understand and wish to continue anyway »

You are using a browser not supported by the Wolfram Cloud. Supported browsers include recent versions of Chrome, Edge, Firefox and Safari.