Add next_generation

resolution.py

@@ -139,6 +139,72 @@ is_false: Callable[[Clause_], bool] = c(p(eq, 0), len)
 """
 Determines whether a clause is equivalent to false
 
+This is only true for the empty clause.
+
+>>> is_false([])
+True
+
+>>> is_false([IRProp('real')])
+False
+"""
+
+def next_generation(
+    previous_generations: KnowledgeBase_,
+    current_generation: KnowledgeBase_,
+) -> KnowledgeBase:
+	"""
+	Advance resolution by one step
+
+	This performs `derive()` on the current generation as well as `derive2()` between the
+	current generation and all clauses from previous generations in order to produce a new
+	generation, hopefully with new and interesting clauses in it.
+
+	When using the new generation, previous generations should be considered to be the sum
+	of all clauses within the two knowledge bases passed to this function.  That is, all
+	clauses which were used in the generation of that generation.
+
+	### Example
+
+	Starting from an example knowledge base, we produce a new generation.  Notice that the
+	empty list for previous generations indicates that this is the zeroth (original)
+	knowledge base.
+
+	>>> next_generation([
+	... ], [
+	...     [IRNeg(IRProp('animal', [IRProp('Kim')]))],
+	...     [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
+	...     [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
+	...     [IRProp('dog', [IRProp('Kim')])],
+	... ]) #doctest: +NORMALIZE_WHITESPACE
+	{
+		{ animal(Kim()) },
+		{ ¬cat(Kim())   },
+		{ ¬dog(Kim())   }
+	}
+
+	Now, we perform the next round of resolution.  All of the terms originally passed into
+	the first generation have been moved to the previous generations knowledge base, and
+	the current generation contains only the results from the first call.
+
+	>>> next_generation([
+	...     [IRNeg(IRProp('animal', [IRProp('Kim')]))],
+	...     [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
+	...     [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
+	...     [IRProp('dog', [IRProp('Kim')])],
+	... ], [
+	...     [IRNeg(IRProp('dog', [IRProp('Kim')]))],
+	...     [IRNeg(IRProp('cat', [IRProp('Kim')]))],
+	...     [IRProp('animal', [IRProp('Kim')])],
+	... ])
+	{ { } }
+
+	The return of a knowledge base containing false (ie `[]`) indicates that resolution
+	has found a contradiction.  In this case, there are two:  One from ¬dog(Kim) and
+	dog(Kim), and one from animal(Kim) and ¬animal(Kim).
+	"""
+	return fset(*derive(current_generation), *derive2(current_generation, previous_generations))
+
+
 if __name__ == '__main__':
 	import doctest
 	doctest.testmod()