Different ways are explored to port PLN to MeTTa. These ways are organized into the following folders:
-
match: rule is represented using MeTTa operator match;
-
entail: rule is represented with the symbol ⊢;
-
backward-chaining: backward chaining experiments, both using proof as program and proof as program execution trace.
-
forward-chainer: forward chainer experiments.
-
forward-chaining: forward chaining experiments, both using proof as program and proof as program execution trace.
-
polyward-chaining: forward chaining experiments combined with backward chaining.
-
hol: higher order logic, attempt to reason about programs, such as providing that 0 is the right identity of +.
-
inference-control: inference control experiments, replace depth by control functions.
-
iterative-chaining: save intermediary results while reasoning.
-
synthesis: program synthesis experiments (backward chaining).
-
subtyping: subtyping inference experiments.
-
sumo: attempt to reason over sumo.
-
common: some reusable type and function definitions.
-
pln: collection of PLN port attempts.
-
equal: rule is represented using MeTTa equality =;
-
dependent-types: rule is represented as type constructor;