a few minor docs site updates

src/SCFirstOrderLogic.Documentation/wwwroot/md/home.md

@@ -7,7 +7,7 @@ Included are:
 
 * Implementations of both raw and CNF sentence representation. 
   Multiple ways of instantiating raw sentences, ranging from string parsing, through a number of code-based approaches, all the way to a language-integrated approach that allows (the domain to be modelled as an IEnumerable<T> and) sentences to be provided as lambda expressions.
-* Knowledge base implementations that, while using very simple (i.e. not production ready) versions of their respective algorithms, do use abstracted, asynchronous clause storage (thus providing an extension point) and expose properties for the retrieval of proof details.
+* Knowledge base implementations that, while using *very* basic (i.e. not production ready) versions of their respective algorithms, do use abstracted, asynchronous clause storage (which could be re-used in more sophisticated knowledge base implementations) and expose properties for the retrieval of proof details.
 * Sentence formatting logic that allows for (customisable) unique labelling of standardised variables and Skolem functions across a set of sentences.
 
 As mentioned above, the main goal here is for it to be a resource for learning and experimentation.

src/SCFirstOrderLogic.Documentation/wwwroot/md/library-overview.md

@@ -14,6 +14,8 @@ Here is a quick overview of the namespaces found within this library. Reading th
   * **`SentenceFormatting`:** logic for creating string representations of sentences. Includes logic for ensuring unique labelling of standardised variables and Skolem functions across a set of sentences.
   * **`SentenceManipulation`:** assorted logic for the manipulation of sentences. Contains some interfaces and base classes for sentence visitors and transformations.
     * **`Unification`:** utility logic for [unifying](https://en.wikipedia.org/wiki/Unification_(computer_science)) literals and sentences.
-  * **`TermIndexing`:** term indexing data structures - there are discrimination tree and path tree implementations in here.
+  * **`TermIndexing`:** term indexing data structures, for fast lookup of generalisations and instances of query terms. 
+    There are discrimination tree and path tree implementations in here.
+    Customisation of the backing store is allowed for via an abstraction for tree nodes, and both synchronous and asynchronous versions exist.
 
 For a full type and member listing, the recommendation is to use the [FuGet package explorer](https://www.fuget.org/packages/SCFirstOrderLogic/) - though going through [getting started](getting-started.md) first is probably a good idea, if you haven't already.

src/SCFirstOrderLogic.Documentation/wwwroot/md/roadmap.md

@@ -5,11 +5,11 @@ I don't intend to add any particularly powerful or specialised inference logic t
 
 Priorities at the time of writing:
 
-* *Easing back on this for the immediate future - working on other stuff.*
+* *Nothing at the moment - working on other projects.*
 
 Further ahead:
 
-* Next up likely to be more indexing stuff - specifically, to facilitate finding subsuming/subsumed clauses.
+* Next up is likely to be more indexing stuff - specifically, to facilitate finding subsuming/subsumed clauses.
   Might go very old-school and build on discrimination/path trees for this, but will probably at least try to go slightly less old-school and have a crack at a feature vector index implementation.
 * Improvements to inference algorithms. As mentioned above and elsewhere, this package is more about the fundamentals than especially powerful inference logic - but we should probably cover at least some of the relatively fundamental problems and techniques - the inference demo is rather underwhelming at the moment.. For example, some or all of:
   * Create a clause store or two that leverages subsumption.