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)
Patterns x_, y_
Substitution
Substitution
Rule with Verbatim pattern LHS
Verbatim[x_]->XXXX
Substitution instance
Substitution instance
MatchQ pair
Unification
Unification
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}
Most General Unifier(s)
Most General Unifier(s)
In[]:=
unify[f[x_,y_],f[x_,x_]]
Out[]=
{x_x_,y_x_}
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, substitutions and cosubstitutions
Premise conclusion
Premise conclusion
Meta-rule input and output
Clauses
Clauses
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
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 and ¬A “annihilate”, expression substitution
Refutational Theorem Proving
Refutational Theorem Proving
Show that {Axioms, ¬ Hypothesis} is inconsistent