First Order/Higher Order Logical Forward reasoning in Mathematica (Mathematica for FOL/HOL knowledge base)?

Question

I am trying to develop Artificial Intelligence system that can automatically discover and apply reasoning patterns, templates, strategies (there is even theory for that - Cognitive Task Analysis). While the details of my effort are in development and they can be discussed (their merit, applicability), I need to accomplish two things and I am now trying to do them with Mathematica. Essentially - these 2 things amount to:

1. Declaration of the FOL/HOL concrete language (knowledge base): I should be able to state in the Mathematica language, that there exist: 1) variables, e.g. x1, x2, etc.; 2) constants, e.g. Peter, John, Mary, etc.; 3) functions, e.g. age(...), child(..., ...), 4) predicates/relations (essentially - boolean-valued functions): isParent(..., ...). For me, it is very important to just state in Mathematica, that such functions (e.g. age(...)) exist and maybe even state the type of their arguments/values but I should not be pressed to define their semantics completely: I intend to define their semantics with the domain axioms and the set of those axioms can be incomplete for determination of the result in some cases. It is quite normal - knowledge bases are filled and updated gradually. Of course, in some cases I can specify the semantics completely - e.g. - in the tabular form or by providing function or even maybe some imperative/functional program (whatever Mathematica allows).

2. Do calculational/forward reasoning on the concrete FOL/HOL language - e.g. compute full or partial consequence set of the knowledge base. The usual approach in the mathematics, Prolog applications, etc., is to hypothesize some formula about the domain knowledge and then ask the system the question - is this formula true, can this formula be derived from the Set theory (e.g. if we are speaking about theorems generally) or the axioms of the knowledge base (e.g. if we are speaking about the concrete domain knowledge base). Essentially this is task of theorem proving or SAT (satisfiability solving). This is backward reasoning. I am trying to do the opposite thing - foward reasoning: my system would like to 1) select premises (e.g. isSmart(Peter), Ax.isSmart(x)->receivesHighWage(x)); 2) select deduction rule (e.g. Modus Ponens https://en.wikipedia.org/wiki/Modus_ponens) and 3) deduce the new formula (e.g. receivesHighWage(Peter)) - result of one reasoning step. I plan, that steps 1 and 2 (the selection of formulas and rule) I will do with my system (it can be Reinforcement Learning system from the Artificial Intelligence - relational or neural, e.g. I can store the Mathematica formulas/premises in my custom graph knowledge base and use neural network to select nodes from the graph database and express those nodes as Mathematica expressions and feed them in the Mathematica engine for doing the 3rd step) but I would like to do the 3rd step - the application of the FOL/HOL deduction rule on the premises - with the Mathematica. Is that possible and how? Any hint is welcome!

So - my question is - can Mathematica be used in the described manner for the declaration of the knowledge base in the First Order Logic or Higher Order Logic? And can Mathematica be used to do just one simple deduction step on such FOL/HOL statements?

It may sound that I am asking two questions in one - declaration and deduction? But essentially it is one question - the implementation of the deduction step apparently greatly depends on the implementation of he KB declaration. So - this is just one question. Maybe this question can be reformulated succinctly as - can Mathematica be used for the implementation of the FOL/HOL knowledge base and how?

Just hints to the relevant Wolfram language constructs and functions is sufficient, I can study Mathematica myself further and write down all the details myself. Thanks!

I am reading https://reference.wolfram.com/language/guide/BooleanComputation.html but there is no hint about declaration of my own functions and there is no hint about the deduction rules, e.g. Modus Ponens.

http://ai4reason.org/activities.html is ongoing work along whose ideas I am trying to develop my own system. One can see that my efforts are quite acceptable, I just only need to know whether Mathematica can be used as medium. AI4Reason project uses mainly proof assistants (Isabelle/HOL and Coq) as their medium, but I am taking more concrete approach and I guess, that Mathematica can be better. Performance can be factor as well - proof assistants can be quite heavy to to providing utmost rigor, Mathematica is just calculator without guarantees of rigor.

Answer 1

I do not understand all you are saying. Try to be a bit less theoretical but more specific.

But maybe you mean something like this:

ClearAll["Global`*"]
peter = {"tall", "smart", "young"};
isSmart[person_] := If[MemberQ[person, "smart"], True, False];
SetAttributes[highWage, HoldFirst]
highWage[person_] := 
 If[isSmart[person] && ! MemberQ[person, "highWadge"], 
  AppendTo[person, "highWadge"]]

peter
highWage[Peter]
peter