TwoWayMultiReplace[{a_<->f[a_]}]
In[]:=
AxiomaticTheoryTWP@AxiomaticTheory["GroupAxioms"]
Out[]=
{a_⊗(b_⊗c_)(a_⊗b_)⊗c_,a_⊗

1
a_,a_⊗
a_


1
}
In FindEquationalProof, internally ∀ quantified variables are converted to pattern variables
Paramodulation?
TwoWayMultiReplaceGraphList[AxiomaticTheoryTWP@AxiomaticTheory["GroupAxioms"]]
FindEquationalProof[]

Skolemization

In[]:=
Exists[x,f[x]]
Out[]=
∃
x
f[x]
In[]:=
Not[Exists[x,f[x]]]==ForAll[x,Not[f[x]]]
Out[]=
True
In[]:=
Not[Exists[x,f[x]]]
Out[]=
∀
x
!f[x]
In[]:=
ForAll[x,Not[f[x]]]
Out[]=
∀
x
!f[x]
FindEquationalProof[]
In[]:=
FindEquationalProof[Exists[x,Mortal[x]],{ForAll[x,Implies[Man[x],Mortal[x]]],Exists[x,Man[x]]}]["ProofDataset"]
Out[]=
Statement
Proof
EquationalizedAxiom
8
(x1&&x2)(x2&&x1)
Input
{{Axiom,1},{Axiom,2}}
EquationalizedHypothesis
1
(
a.
0
||!
a.
0
)Mortal[
EquationalProof`c
1
]
Input
{{Hypothesis,1}}
CriticalPairLemma
1
((x1&&!x1)||x2)x2
Construct
{EquationalizedAxiom,3}
Orientation
{-1,1}
9 total ›
CriticalPairLemma
2
(x1||(x2&&!x1))(x1||x2)
Construct
{EquationalizedAxiom,4}
Orientation
-1
9 total ›
CriticalPairLemma
3
(x1&&(x2||!x1))(x1&&x2)
Construct
{EquationalizedAxiom,5}
Orientation
1
9 total ›
SubstitutionLemma
1
(Mortal[x1]||!Man[x1])(
a.
0
||!
a.
0
)
Input
{EquationalizedAxiom,6}
Position
1
6 total ›
SubstitutionLemma
2
(Mortal[ELProver`Const2]||!Man[ELProver`Const2])Man[
EquationalProof`c
1
]
Input
{EquationalizedAxiom,7}
Position
1
6 total ›
CriticalPairLemma
4
((x1||!x1)&&x2)x2
Construct
{EquationalizedAxiom,8}
Orientation
{-1,1}
9 total ›
CriticalPairLemma
5
(x1&&x2)(x1&&(!x1||x2))
Construct
{CriticalPairLemma,1}
Orientation
1
9 total ›
CriticalPairLemma
6
(x1||x2)(x1||(!x1&&x2))
Construct
{CriticalPairLemma,4}
Orientation
1
9 total ›
rows 11–20 of
41
Introducing Skolem constants
Exists[x,f[x]]
is replaced by
f[c]
for some c
Trying to prove satisfiability for a symbolic c is the same as saying there exists a c

Paramodulation

Multiway Math

In[]:=
AxiomaticTheoryTWP@AxiomaticTheory["GroupAxioms"]
Out[]=
{a_⊗(b_⊗c_)(a_⊗b_)⊗c_,a_⊗

1
a_,a_⊗
a_


1
}
In[]:=
TwoWayMultiReplaceGraphList[AxiomaticTheoryTWP@AxiomaticTheory["GroupAxioms"]]
Out[]=

,

In[]:=
VertexList/@%
Out[]=
{a_⊗(b_⊗c_)(a_⊗b_)⊗c_,a_⊗

1
a_,a_⊗
a_


1
},a_⊗(b_⊗c_)(a_⊗b_)⊗c_,(a_⊗b_)⊗c_(a_⊗b_)⊗c_,a_⊗(b_⊗c_)a_⊗(b_⊗c_),a_⊗

1
a_,a_⊗
a_


1
,(a_⊗

1
)⊗(b_⊗c_)(a_⊗b_)⊗c_,a_⊗((b_⊗

1
)⊗c_)(a_⊗b_)⊗c_,a_⊗(b_⊗(c_⊗

1
))(a_⊗b_)⊗c_,a_⊗((b_⊗c_)⊗

1
)(a_⊗b_)⊗c_,(a_⊗(b_⊗c_))⊗

1
(a_⊗b_)⊗c_,a_⊗(b_⊗c_)((a_⊗

1
)⊗b_)⊗c_,a_⊗(b_⊗c_)(a_⊗(b_⊗

1
))⊗c_,a_⊗(b_⊗c_)((a_⊗b_)⊗

1
)⊗c_,a_⊗(b_⊗c_)(a_⊗b_)⊗(c_⊗

1
),a_⊗(b_⊗c_)((a_⊗b_)⊗c_)⊗

1
,a_a_,(a_⊗

1
)⊗

1
a_,a_⊗

1⊗

1
a_,a_⊗(

1
⊗

1
)a_,a_⊗

1
a_⊗

1
,(a_⊗

1
)⊗
a_


1
,a_⊗
a_⊗

1


1
,a_⊗(
a_
⊗

1
)

1
,(a_⊗
a_
)⊗

1


1
,a_⊗
a_


1⊗

1
,a_⊗
a_


1
⊗

1
,a_⊗(b_⊗
b_
)a_,

1


1
,a_⊗
a_
b_⊗
b_

In[]:=
Reverse[a_⊗
a_


1
]
Out[]=

1
a_⊗
a_

1
⊗

1
Generated variables??

1
⊗

1
In[]:=
TwoWayMultiReplaceGraphList[AxiomaticTheoryTWP@AxiomaticTheory["GroupAxioms"],2]
In[]:=
TwoWayMultiReplaceGraphList[{a_⊗
a_


1
},2]
Out[]=

,
,

In[]:=
VertexList/@%
Out[]=
{{a_⊗
a_


1
},{a_⊗
a_


1
,

1


1
,a_⊗
a_
b_⊗
b_
},{a_⊗
a_


1
,

1


1
,a_⊗
a_
b_⊗
b_
,b_⊗
b_
a_⊗
a_
,

1
a_⊗
a_
}}
Knitting by variables?? Or are variables always unique atoms??
In[]:=
TwoWayMultiReplaceGraphList[{a_⊗
a_


1
},3]

Minimal Case

Critical pair lemma is knitting together two 2-way rules
Critical pairs come from branchially separated events

Types of events

1 . Substitution lemma 2-way + 2 way  2-way [substitutions could be applied in more than one way]
2. Critical pair lemma 2-way + 2 way  2-way [cpl can be applied in more than one way]
This rule application is to position 1, not e.g. {1,1,1} ... in other words to the outermost f not e.g. the innermost
There is a meta-rule in FEP which say x_ == x_ for any x gives the “True” conclusion [apparently comes from paramodulation]
This does not contain the f[f[a]]↔a from FEP
Paramodulation: ~ canonicalization when applied to expressions (cf variable renaming)
Paramodulation is a way of burning in certain base axioms (specifically, axioms of equality)
​