Try to use Metatheory.jl in a Reasoning System.

[AIxer]

Hi, I am working on a Reasoning System, it has some syllogistic rules like:

"""
{<S --> M>, <M -->P>} |- <S --> P>
{<S ==> M>, <M ==>P>} |- <S ==> P>
{<P --> T>, (*, P, S)} |- <(*,P,S) --> T>
...
"""

complete rules in Prolog: nal.pl
what I'm doing now:

abstract type Term end

struct Atom <: Term
    val::Symbol
end

struct Inheritance <: Term
    comps::Vector{Term}
end

function dispatch(term1, term2, ...)
    # a big switch table
    if ...
        ...
    elseif ...
        ...
    elseif ...
        deduction(term1, term2) # OK find a suitable rule
    end
end

function deduction(term1::Inheritance, term2::Inheritance)
    conclusion = if term1[2] == term2[1]
        Inheritance(term1[1], temr2[2])
    elseif term1[1] = term2[2]
        ...
    elseif term1[1] = term2[1]
        ...
    elseif term1[2] == term2[2]
        ...
    end
end

Are there ways to make it simple? the old way above is just rule translation.
This is another implementation uses C macro:

//!Consequent substitutions
R2( (A =/> B), (S ==> B), |-, (A =/> S), Truth_Induction )
R2( (A =/> (P --> B)), (P <-> S), |-, (A =/> (S --> B)), Truth_Analogy )
R2( (A =/> (B --> P)), (P <-> S), |-, (A =/> (B --> S)), Truth_Analogy )
//!First sequence element substitution (deeper isn't currently linked)
R2( ((A &/ B) =/> C), (A ==> S), |-, ((S &/ B) =/> C), Truth_Induction )
R2( ((A &/ B) =/> C), (S ==> A), |-, ((S &/ B) =/> C), Truth_Deduction )
#endif

Is there a declarative way in Metatheory.jl to achieve this?