Enum InferenceRule 

pub enum InferenceRule {
    PremiseMatch,
    ModusPonens,
    ModusTollens,
    ConjunctionIntro,
    ConjunctionElim,
    DisjunctionIntro,
    DisjunctionElim,
    DoubleNegation,
    UniversalInst(String),
    UniversalIntro {
        variable: String,
        var_type: String,
    },
    ExistentialIntro {
        witness: String,
        witness_type: String,
    },
    ModalAccess,
    ModalGeneralization,
    TemporalTransitivity,
    StructuralInduction {
        variable: String,
        ind_type: String,
        step_var: String,
    },
    Rewrite {
        from: ProofTerm,
        to: ProofTerm,
    },
    EqualitySymmetry,
    EqualityTransitivity,
    Reflexivity,
    Axiom,
    OracleVerification(String),
    ReductioAdAbsurdum,
    Contradiction,
    ExistentialElim {
        witness: String,
    },
    CaseAnalysis {
        case_formula: String,
    },
}

The “Lever” - The specific logical move made at each proof step.

This enum captures HOW we moved from premises to conclusion. Each variant corresponds to a different proof strategy or logical rule.

See Also

• DerivationTree - Each node contains an InferenceRule
• certifier::certify - Maps inference rules to kernel terms
• hints::suggest_hint - Suggests applicable rules when stuck
• BackwardChainer - The engine that selects and applies rules

Variants

PremiseMatch

Direct match with a known fact in the Context/KnowledgeBase. Logic: Γ, P ⊢ P

ModusPonens

Logic: P → Q, P ⊢ Q

ModusTollens

Logic: ¬Q, P → Q ⊢ ¬P

ConjunctionIntro

Logic: P, Q ⊢ P ∧ Q

ConjunctionElim

Logic: P ∧ Q ⊢ P (or Q)

DisjunctionIntro

Logic: P ⊢ P ∨ Q

DisjunctionElim

Logic: P ∨ Q, P → R, Q → R ⊢ R

DoubleNegation

Logic: ¬¬P ⊢ P (and P ⊢ ¬¬P)

UniversalInst(String)

Logic: ∀x P(x) ⊢ P(c) Stores the specific term ‘c’ used to instantiate the universal.

UniversalIntro

Logic: Γ, x:T ⊢ P(x) implies Γ ⊢ ∀x:T. P(x) Stores variable name and type name for Lambda construction.

Fields

variable: String

var_type: String

ExistentialIntro

Logic: P(w) ⊢ ∃x.P(x) Carries the witness and its type for kernel certification.

Fields

witness: String

witness_type: String

ModalAccess

Logic: □P (in w0), Accessible(w0, w1) ⊢ P (in w1) “Necessity Elimination” / “Distribution”

ModalGeneralization

Logic: If P is true in ALL accessible worlds ⊢ □P “Necessity Introduction”

TemporalTransitivity

Logic: t1 < t2, t2 < t3 ⊢ t1 < t3

StructuralInduction

Logic: P(0), ∀k(P(k) → P(S(k))) ⊢ ∀n P(n) Stores the variable name, its inductive type, and the step variable used.

Fields

variable: String

ind_type: String

step_var: String

Rewrite

Leibniz’s Law / Substitution of Equals Logic: a = b, P(a) ⊢ P(b) The equality proof is in premise\[0\], the P(a) proof is in premise\[1\]. Carries the original term and replacement term for certification.

Fields

from: ProofTerm

to: ProofTerm

EqualitySymmetry

Symmetry of Equality: a = b ⊢ b = a

EqualityTransitivity

Transitivity of Equality: a = b, b = c ⊢ a = c

Reflexivity

Reflexivity of Equality: a = a (after normalization) Used when both sides of an identity reduce to the same normal form.

Axiom

“The User Said So.” Used for top-level axioms.

OracleVerification(String)

“The Machine Said So.” (Z3 Oracle) The string contains the solver’s justification.

ReductioAdAbsurdum

Proof by Contradiction (Reductio ad Absurdum) Logic: Assume ¬C, derive P ∧ ¬P (contradiction), conclude C Or: Assume P, derive Q ∧ ¬Q, conclude ¬P

Contradiction

Contradiction detected in premises: P and ¬P both hold Logic: P, ¬P ⊢ ⊥ (ex falso quodlibet)

ExistentialElim

Existential Elimination (Skolemization in a proof context) Logic: ∃x.P(x), [c fresh] P(c) ⊢ Goal implies ∃x.P(x) ⊢ Goal The witness c must be fresh (not appearing in Goal).

Fields

witness: String

CaseAnalysis

Case Analysis (Tertium Non Datur / Law of Excluded Middle) Logic: (P → ⊥), (¬P → ⊥) ⊢ ⊥ Used for self-referential paradoxes like the Barber Paradox.

Fields

case_formula: String

Trait Implementations

impl Clone for InferenceRule

fn clone(&self) -> InferenceRule

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for InferenceRule

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for InferenceRule

fn eq(&self, other: &InferenceRule) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for InferenceRule