Theorem proving jargon to WL dictionary
Terms
Terms
Expressions with patterns (free of predicates)
Predicates
Predicates
Special head symbols (formal symbol, string or logical connective)
Function symbols
Function symbols
Other symbol heads
Atomic formulas/Atomic sentences/Atoms
Atomic formulas/Atomic sentences/Atoms
Expressions with predicate heads
Variables (First-order logic)
Variables (First-order logic)
Universal quantifier ForAll
Patterns x_, y_
Patterns x_, y_
Substitution
Substitution
Rule with Verbatim pattern LHS
Verbatim[x_]->XXXX
Substitution instance
Substitution instance
MatchQ pair
Unification
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)
Most General Unifier(s)
In[]:=
unifier[f[x_,y_],f[x_,x_]]
Out[]=
{y_x_,x_y_}
Ground atoms
Ground atoms
No patterns
Logical connectives
Logical connectives
Equivalence (≡, ⇔): TwoWayRule
Implication (): Rule
Disjunction (∨): Alternatives, Except[LHS] RHS
Conjunction (∧): meta-rule LHS
Not (¬): ¬A, ¬A ∨ ⊥, A ⊥
True (⊤): ⊤, ⊤ ∨ ⊥, ⊥ ⊥, ⊥ ⇔ ⊥
False (⊥): ⊤ ⊥
Implication (): Rule
Disjunction (∨): Alternatives, Except[LHS] RHS
Conjunction (∧): meta-rule LHS
Not (¬): ¬A, ¬A ∨ ⊥, A ⊥
True (⊤): ⊤, ⊤ ∨ ⊥, ⊥ ⊥, ⊥ ⇔ ⊥
False (⊥): ⊤ ⊥
Inference
Inference
Meta-rules, events, like substitutions and cosubstitutions
Premise conclusion
Premise conclusion
Meta-rule input and output
Clauses (in Conjunctive Normal Form)
Clauses (in Conjunctive Normal Form)
Tokens
Standard clause - Predicate tokens
General clause - Predicate tokens + Term tokens
Standard clause - Predicate tokens
General clause - Predicate tokens + Term tokens
(Herbrand) interpretation
(Herbrand) interpretation
Set of true ground tokens
Model
Model
True ground token
Consistency
Consistency
Model exists
Contradiction
Contradiction
Inconsistent expression without function and predicate symbols (only logical connectives)
Proof
Proof
Sequence of clauses (assumptions)
Refutation
Refutation
Derive contradiction
Saturation
Saturation
Fixed point
Redundancy criterion
Redundancy criterion
RuleSelectionFunction
Deduction
Deduction
Adding tokens
Derivation
Derivation
Adding and deleting tokens
Narrowing
Narrowing
Forbid inferences at positions of already existing (functional) tokens
Resolution
Resolution
A∨B∨C
&
¬A∨D∨E
__________
B∨C∨D∨E
&
¬A∨D∨E
__________
B∨C∨D∨E
AB(¬A∨B)⇔(AB)
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)
Or A and ¬B “annihilate” after unifying A and B
Which is just what MapAt[Replace] or ReplaceAt naturally do (usual expression substitution)
In[]:=
Out[]=
f[h[b,a],c]
Rule seen as implication is just a disjunction . and “annihilate” after unification:
g[x_,y_]->h[y,x]
Except[g[x_,y_]]|h[y_,x_]
Except[g[x_,y_]]
g[a,b]
In[]:=
unifier[g[x_,y_],g[a,b]]
Out[]=
y_b,x_a
h[b,a]
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
Paramodulation
s==t , E[u]
_______
E[v]
_______
E[v]
Para-substitution for equational formula (aka critical pair computation).
Demodulation
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_⊗1a_,a_⊗1,11,11⊗,1((a_⊗b_)⊗c_)⊗,1(a_⊗1)⊗,1(a_⊗(b_⊗c_))⊗,1(a_⊗)⊗1,1(a_⊗)⊗,1(a_⊗b_)⊗,1⊗a_,1a_⊗(⊗1),1a_⊗,1a_⊗,1⊗1a_⊗,1⊗(a_⊗b_)((c_⊗)⊗a_)⊗b_,1⊗a_a_⊗(b_⊗),1⊗a_a_,1⊗b_a_⊗(⊗b_),(1⊗b_)⊗c_(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_)⊗1a_⊗(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)⊗1a_,(a_⊗1)⊗(b_⊗c_)(a_⊗b_)⊗c_,(a_⊗1)⊗b_b_⊗a_,(a_⊗1)⊗c_a_⊗((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_⊗))⊗b_a_⊗(1⊗b_),(a_⊗(c_⊗b_))⊗d_a_⊗((b_⊗c_)⊗d_),(a_⊗)⊗b_b_⊗1,(a_⊗b_)⊗1a_⊗(b_⊗(c_⊗)),(a_⊗b_)⊗1a_⊗b_,(a_⊗b_)⊗1b_⊗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_⊗)a_⊗(b_⊗1),(a_⊗b_)⊗(c_⊗d_)a_⊗((b_⊗c_)⊗d_),(a_⊗b_)⊗(d_⊗c_)a_⊗(b_⊗(c_⊗d_)),(a_⊗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_⊗)⊗a_a_⊗1,(b_⊗a_)⊗1a_⊗b_,(b_⊗a_)⊗c_a_⊗(b_⊗c_),(c_⊗b_)⊗a_a_⊗(b_⊗c_),a_⊗1a_⊗1,a_⊗(1⊗1)a_,a_⊗(1⊗b_)a_⊗b_,a_⊗(b_⊗1)b_⊗a_,a_⊗(b_⊗)a_,a_⊗(b_⊗c_)a_⊗(b_⊗c_),a_⊗(b_⊗c_)b_⊗(c_⊗a_),a_⊗(b_⊗c_)c_⊗(a_⊗b_),a_⊗b_⊗,a_⊗b_a_⊗b_,a_⊗b_b_⊗(a_⊗1),a_a_
a_
a_⊗
a_
a_⊗(b_⊗c_)
a_
(a_⊗b_)⊗c_
a_
a_
1
b_⊗a_
a_
a_
a_⊗1
a_
a_
c_
b_
a_
a_
b_
c_
a_
c_
c_
b_
b_
b_
a_
b_
Variable renaming
Variable renaming
Resolution should always be done with variable renaming
Refutational Theorem Proving
Refutational Theorem Proving
Show that {Axioms, ¬ Hypothesis} is inconsistent
Clausal (prenex) form
Clausal (prenex) form
First-order logic formula can be turned into a list of rules
Skolemization
Skolemization
Remove existential quantifies by introducing new function symbols
Proof justification
Proof justification
ProofDataset entry tuple (input, position, construct, orientation, rule, output)
Usually (input, output, lhs, rhs, substitution, position)
Usually (input, output, lhs, rhs, substitution, position)
Peak
Peak
Branch-pair
Reduction ordering
Reduction ordering
Well-founded
Stable
Monotonic
Stable
Monotonic
Knuth-Bendix completion
Knuth-Bendix completion
Cut-elimination
Cut-elimination
FindEquationalProof FindReplacePath