a family of inference algorithm which acts over definite clauses. these algorithms work backward from the goal, chaining through rules to find own facts that support the proof.
a family of inference algorithm which acts over definite clauses. these algorithms work backward from the goal, chaining through rules to find own facts that support the proof.