Can Metatheory.jl work functional equal to Prolog?

I’m rewriting a Reasoning System using Julia. The system has many rules written in Prolog, I want to use these existing prolog rules, because they are declarative and could make the whole system easy to debug it’s control mechanism without care much about its reasoning process.

In theory.

Sounds like a warning (or a play of words).

yeah, the reasoning system does syllogism.
It has some rules like:

# two premises, one or more conclusions.
{M --> P, S --> M} |- S --> P  # deduction
{S --> M, M --> P} |- S --> P, P --> S, P <-> S  # exemplification
{S --> M, P --> M} |- (&,S,P) --> M

# translate into prolog style
infer(inheritance(S,M), inheritance(M,P), inheritance(S,P)).

I’m trying to replace Julog.jl with Metatheory.jl in the system that I’m rewritting in Julia.

Well, I think this might be over my head.

Experiment:

abstract type MyTerm end
struct Inheritance <: MyTerm
    comps::Vector{MyTerm}
end

struct Similarity <: MyTerm
    comps::Vector{MyTerm}
end

struct Word <: MyTerm
    sym::Symbol
end

inheritance(a, b) = Inheritance([Word(a), Word(b)])
similarity(a, b) = Similarity([Word(a), Word(b)])

syllogism = @theory S M P begin
    inheritance(S, M) + inheritance(M, P) => inheritance(S, P)
    inheritance(S, M) + inheritance(M, P) => Inheritance([Word(P), Word(S)]);
    inheritance(S, M) + inheritance(M, P) => Similarity([Word(S), Word(P)]);
    # prolog-like
    infer(inheritance(S, M), inheritance(M, P)) --> similarity(P, S);
    # more rules ...
end

rewrite(:(inheritance(s, m) + inheritance(m, p)), syllogism)

Great! But it seems only rewrite once.

julia> rewrite(:(inheritance(s, m) + inheritance(m, p)), syllogism)
Inheritance(MyTerm[Word(:s), Word(:p)])

I need to learn more about Metatheory.jl ! :grinning:

You might be interested in this package:

https://github.com/ztangent/Julog.jl

Yes,I’m using it in current project. Thx! :grin: