Prove a goal against a knowledge base and return every solution with its proof.

Use this for any question that needs multi-step deduction over facts and rules: transitive relations, permission inheritance, property inheritance, eligibility checks, or filtering a large fact set by a rule.

The goal comes from the query parameter, or from the ? ... line(s) in knowledge when query is omitted.

Returns ReasonResult:

• ok (bool): false when the request could not be evaluated.

• solutions (list): each has bindings (list of {var, value}, empty for a ground yes/no query), proof (a tree of {goal, type, children} where type is fact, rule or and), and proof_text (the tree rendered as indented text).

• solution_count (int): how many solutions are returned.

• truncated (bool): true when more solutions existed than max_solutions.

• error (str | null): a readable, actionable message when ok is false.

An empty solutions list with ok: true means the goal is false under closed-world semantics - the knowledge base does not entail it.

Explain why a query holds, why it fails, or what would make it true.

Reach for this when reason returns something you did not expect. Modes:

• why: the goal holds and you want the derivation.

• why_not: the goal fails and you want the missing facts or rules named. Reports predicates with no definition at all, then the deepest sub-goals that could not be proved.

• what_needs: the goal fails and you want the smallest set of facts that would make it true (bounded to 3 assumptions over base predicates).

Returns DiagnosisResult:

• ok (bool): false when the request could not be evaluated.

• holds (bool): whether the goal currently holds.

• findings (list of str): observations, most actionable first.

• conclusion (str): a human-readable summary; for why it includes the rendered derivation.

• proof (object | null): the derivation tree, present when the goal holds.

• error (str | null): a readable message when ok is false.

Apply hypothetical fact changes and compare the query before and after.

Use this to test a change without committing to it: promoting a user to a role, adding a resource, revoking an assignment. modifications is one change per line, + fact(...) to add or - fact(...) to remove. Only facts can be changed, not rules. A - line that matches no existing fact is an error, so a typo cannot silently produce a misleading comparison.

Returns WhatIfResult:

• ok (bool): false when the request could not be evaluated.

• before_count, after_count (int): solution counts on each knowledge base.

• delta (int): after_count - before_count.

• solutions_before, solutions_after (list): full solutions with proofs.

• applied (list of str): the modifications as applied, normalized.

• conclusion (str): a readable description of the impact.

• error (str | null): a readable message when ok is false.

Validate a knowledge base statically, without running it.

Cheap and backend-free: call it before reason when you have just written or edited a knowledge base. It catches syntax errors, predicates used but never defined, recursion with no base case, and duplicate facts or rules.

Returns KBCheckResult:

• valid (bool): false only when the knowledge base does not parse.

• errors (list of str): parse failures, with line and column.

• warnings (list of str): undefined predicates, possible non-termination, duplicates. Warnings do not prevent reasoning.

• facts_count, rules_count (int): items found.

• predicates_count (int): distinct name/arity predicate symbols.