Try to use Metatheory.jl in a Reasoning System.
AIxer opened this issue · 0 comments
AIxer commented
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?