Theorem proving jargon to WL dictionary
https://www.cs.unm.edu/~mccune/prover9/manual/2009-11A/glossary.html#

Terms

Expressions with patterns (free of predicates)

Predicates

Special head symbols (formal symbol, string or logical connective)

Function symbols

Other symbol heads

Atomic formulas/Atomic sentences/Atoms

Expressions with predicate heads

Variables (First-order logic)

Universal quantifier ForAll
Patterns x_, y_

Substitution

Rule with Verbatim pattern LHS
Verbatim[x_]->XXXX

Substitution instance

MatchQ pair

Unification

Matching of expressions. Turn MatchQ pair into a list of (Verbatim) pattern replacement rules
In[]:=
MatchQ[f[a,b],f[___,x_,y___]]
Out[]=
True
In[]:=
f[___,x_,y___]/.{Verbatim[x_]->a,Verbatim[y___]->b}
Out[]=
f[___,a,b]
In[]:=
unify[f[___,x___,y_],f[a,b]]
Out[]=
{x___a,y_b,x___Sequence[],y_b}
In[]:=
unify[f[OrderlessPatternSequence[x_,y_]],f[a,b]]
Out[]=
{x_a,y_b,x_b,y_a}
Two directions of unification produce two cases for performing expression replacement: substitutions and cosubstitutions (c.f. paramodulation)
In[]:=
substitutionLemmas[f[x_,z_],f[x_,y_]->g[x_,y_,z_],"Uniquify"->True]
Out[]=
{{{}},1}g[x_,z_,z$237_]
In[]:=
coSubstitutionLemmas[f[x_,z_],f[x_,y_]->g[x_,y_,z_],"Uniquify"->True]
Out[]=
{{{}},1}g[x$236_,y$237_,z$238_],{{{1}},1}f[g[x$236_,y$237_,z$238_],z_],{{{2}},1}f[x_,g[x$236_,y$237_,z$238_]]

Most General Unifier(s)

In[]:=
unifier[f[x_,y_],f[x_,x_]]
Out[]=
{y_x_,x_y_}

Ground atoms

No patterns

Logical connectives

Equivalence (≡, ⇔): TwoWayRule
Implication (): Rule
Disjunction (∨): Alternatives, Except[LHS]  RHS
Conjunction (∧): meta-rule LHS
Not (¬): ¬A, ¬A ∨ ⊥, A  ⊥
True (⊤): ⊤, ⊤ ∨ ⊥, ⊥  ⊥, ⊥ ⇔ ⊥
False (⊥): ⊤  ⊥

Inference

Meta-rules, events, like substitutions and cosubstitutions

Premise  conclusion

Meta-rule input and output

Clauses (in Conjunctive Normal Form)

Tokens
Standard clause - Predicate tokens
General clause - Predicate tokens + Term tokens

(Herbrand) interpretation

Set of true ground tokens

Model

True ground token

Consistency

Model exists

Contradiction

Inconsistent expression without function and predicate symbols (only logical connectives)

Proof

Sequence of clauses (assumptions)

Refutation

Derive contradiction

Saturation

Fixed point

Redundancy criterion

RuleSelectionFunction

Deduction

Adding tokens

Derivation

Adding and deleting tokens

Narrowing

Forbid inferences at positions of already existing (functional) tokens

Resolution

A∨B∨C
&
¬A∨D∨E
__________
B∨C∨D∨E
AB​​(¬A∨B)⇔(AB)
A and ¬A “annihilate”
Or A and ¬B “annihilate” after unifying A and B
​
Which is just what MapAt[Replace] or ReplaceAt naturally do (usual expression substitution)
In[]:=
[◼]
ReplaceAt
[f[g[a,b],c],g[x_,y_]->h[y,x],{1}]
Out[]=
f[h[b,a],c]
Rule
g[x_,y_]->h[y,x]
seen as implication is just a disjunction
Except[g[x_,y_]]|h[y_,x_]
.
Except[g[x_,y_]]
and
g[a,b]
“annihilate” after unification:
In[]:=
unifier[g[x_,y_],g[a,b]]
Out[]=
y_b,x_a
h[b,a]
is what left (at given position)
In[]:=
substitutionLemmas[f[g[a,b],c],g[x_,y_]->h[y,x]]
Out[]=
{{{1}},1}f[h[y,x],c]
Or Co-substitution if unification happens in opposite direction.
In[]:=
coSubstitutionLemmas[f[g[x_,y_],y_,x_],g[a_,b]->h[b,a]]
Out[]=
{{{1,1}},1}f[g[h[b,a],y_],y_,g[a$8_,b]],{{{1,2}},1}f[g[x_,h[b,a]],g[a$8_,b],x_],{{{1}},1}f[h[b,a],b,a$8_],{{{2}},1}f[g[x_,g[a$8_,b]],h[b,a],x_],{{{3}},1}f[g[g[a$8_,b],y_],y_,h[b,a]]
Three kinds of replacements:
In[]:=
MultiReplace[{f[a,b],f[y_,x_],f[a,x_]},f[y_,b]->c,,"InnerMatch"->_f->_]​​MultiCoReplace[{f[a,b],f[y_,x_],f[a,x_]},f[y_,b]->c,"InnerMatch"->_f->_]​​MultiParaReplace[{f[a,b],f[y_,x_],f[a,x_]},f[y_,b]->c,"InnerMatch"->_f->_]
Out[]=
{{1}}{{c,f[y_,x_],f[a,x_]}}
Out[]=
{{2}}{{f[a,b],c,f[a,b]}}
Out[]=
{{1}}{{c,f[y_,x_],f[a,x_]}},{{2}}{{f[a,b],c,f[a,b]}},{{3}}{{f[a,b],f[y_,b],c}}

Paramodulation

s==t , E[u]
_______
E[v]
Para-substitution for equational formula (aka critical pair computation).

Demodulation

Discard simple tokens that match already present
In[]:=
vs=VertexList[AccumulativeTokenEventGraph[patternify[AxiomaticTheory["AbelianGroupAxioms"]]/.OverTilde->Identity,1],_TwoWayRule]
Out[]=
a_⊗(b_⊗c_)(a_⊗b_)⊗c_,a_⊗b_b_⊗a_,a_⊗1a_,a_⊗
a_
1,11,11⊗
a_⊗
a_
,1((a_⊗b_)⊗c_)⊗
a_⊗(b_⊗c_)
,1(a_⊗1)⊗
a_
,1(a_⊗(b_⊗c_))⊗
(a_⊗b_)⊗c_
,1(a_⊗
a_
)⊗1,1(a_⊗
a_
)⊗
1
,1(a_⊗b_)⊗
b_⊗a_
,1
a_
⊗a_,1a_⊗(
a_
⊗1),1a_⊗
a_⊗1
,1a_⊗
a_
,1⊗1a_⊗
a_
,1⊗(a_⊗b_)((c_⊗
c_
)⊗a_)⊗b_,1⊗a_a_⊗(b_⊗
b_
),1⊗a_a_,1⊗b_a_⊗(
a_
⊗b_),(1⊗b_)⊗c_(a_⊗
a_
)⊗(b_⊗c_),(((a_⊗b_)⊗c_)⊗d_)⊗e_(a_⊗(b_⊗c_))⊗(d_⊗e_),((a_⊗1)⊗b_)⊗c_a_⊗(b_⊗c_),((a_⊗(b_⊗c_))⊗d_)⊗e_((a_⊗b_)⊗c_)⊗(d_⊗e_),((a_⊗b_)⊗1)⊗c_a_⊗(b_⊗c_),((a_⊗b_)⊗c_)⊗1a_⊗(b_⊗c_),((a_⊗b_)⊗c_)⊗d_a_⊗((b_⊗c_)⊗d_),((a_⊗b_)⊗c_)⊗d_d_⊗(a_⊗(b_⊗c_)),((b_⊗a_)⊗c_)⊗d_(a_⊗b_)⊗(c_⊗d_),((b_⊗c_)⊗d_)⊗a_a_⊗(b_⊗(c_⊗d_)),(a_⊗1)⊗1a_,(a_⊗1)⊗(b_⊗c_)(a_⊗b_)⊗c_,(a_⊗1)⊗b_b_⊗a_,(a_⊗1)⊗c_a_⊗((b_⊗
b_
)⊗c_),(a_⊗((b_⊗c_)⊗d_))⊗e_a_⊗((b_⊗(c_⊗d_))⊗e_),(a_⊗(b_⊗1))⊗c_a_⊗(b_⊗c_),(a_⊗(b_⊗(c_⊗d_)))⊗e_a_⊗(((b_⊗c_)⊗d_)⊗e_),(a_⊗(b_⊗c_))⊗1(a_⊗b_)⊗c_,(a_⊗(b_⊗c_))⊗d_(a_⊗b_)⊗(c_⊗d_),(a_⊗(b_⊗c_))⊗d_a_⊗(b_⊗(c_⊗d_)),(a_⊗(b_⊗c_))⊗d_d_⊗((a_⊗b_)⊗c_),(a_⊗(c_⊗
c_
))⊗b_a_⊗(1⊗b_),(a_⊗(c_⊗b_))⊗d_a_⊗((b_⊗c_)⊗d_),(a_⊗
a_
)⊗b_b_⊗1,(a_⊗b_)⊗1a_⊗(b_⊗(c_⊗
c_
)),(a_⊗b_)⊗1a_⊗b_,(a_⊗b_)⊗1b_⊗a_,(a_⊗b_)⊗((c_⊗d_)⊗e_)a_⊗(b_⊗(c_⊗(d_⊗e_))),(a_⊗b_)⊗(c_⊗1)a_⊗(b_⊗c_),(a_⊗b_)⊗(c_⊗(d_⊗e_))a_⊗(b_⊗((c_⊗d_)⊗e_)),(a_⊗b_)⊗(c_⊗
c_
)a_⊗(b_⊗1),(a_⊗b_)⊗(c_⊗d_)a_⊗((b_⊗c_)⊗d_),(a_⊗b_)⊗(d_⊗c_)a_⊗(b_⊗(c_⊗d_)),(a_⊗b_)⊗
b_
a_⊗1,(a_⊗b_)⊗c_(a_⊗b_)⊗c_,(a_⊗b_)⊗c_(b_⊗c_)⊗a_,(a_⊗b_)⊗c_(c_⊗a_)⊗b_,(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_),(a_⊗b_)⊗c_c_⊗(b_⊗a_),(a_⊗c_)⊗b_a_⊗(b_⊗c_),(b_⊗1)⊗a_a_⊗b_,(b_⊗(c_⊗d_))⊗a_a_⊗((b_⊗c_)⊗d_),(b_⊗
b_
)⊗a_a_⊗1,(b_⊗a_)⊗1a_⊗b_,(b_⊗a_)⊗c_a_⊗(b_⊗c_),(c_⊗b_)⊗a_a_⊗(b_⊗c_),a_⊗1a_⊗1,a_⊗(1⊗1)a_,a_⊗(1⊗b_)a_⊗b_,a_⊗(b_⊗1)b_⊗a_,a_⊗(b_⊗
b_
)a_,a_⊗(b_⊗c_)a_⊗(b_⊗c_),a_⊗(b_⊗c_)b_⊗(c_⊗a_),a_⊗(b_⊗c_)c_⊗(a_⊗b_),a_⊗
a_
b_⊗
b_
,a_⊗b_a_⊗b_,a_⊗b_b_⊗(a_⊗1),a_a_

Variable renaming

Resolution should always be done with variable renaming

Refutational Theorem Proving

Show that {Axioms, ¬ Hypothesis} is inconsistent

Clausal (prenex) form

First-order logic formula can be turned into a list of rules

Skolemization

Remove existential quantifies by introducing new function symbols

Proof justification

ProofDataset entry tuple (input, position, construct, orientation, rule, output)
Usually (input, output, lhs, rhs, substitution, position)

Peak

Branch-pair

Reduction ordering

Well-founded
Stable
Monotonic

Knuth-Bendix completion

Cut-elimination

FindEquationalProof  FindReplacePath