Reasoning

Answers can carry more than bindings. These pages cover matching that is a judgment rather than a yes or no: matchers you write yourself, and the measure algebra that scores, orders, and samples what they return.

• Custom matching gives grounded values their own matching logic inside unify.
• Weighted relations answers classes with weights as annotations, on the general surface.

Soft unification, proof search that scores structural closeness, grew into its own library and lives in the sibling pettaprove repository.