README.md

Chaining Experiments in MeTTa

backward-chaining: backward chaining experiments, both using proof as program and proof as program execution trace.
common: some reusable type and function definitions.
converters: functions to convert rule formats, such as curried to uncurried, dependent types to functional.
curried-chaining: backward and forward chaining experiments using curried rules.
forward-chaining: forward chaining experiments, both using proof as program and proof as program execution trace.
program-verification: 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.
pln: collection of PLN port attempts.
polyward-chaining: forward chaining experiments combined with backward chaining.
proof-tree: displaying proof tree, as well as generating fully annotated proof tree.
subtyping: subtyping inference experiments.
sumo: attempt to reason over sumo.
synthesis: program synthesis experiments, actually uncurried backward chaining experiment.