Static analysis message resolutions, and an XML doc improvement.

src/SCFirstOrderLogic/CNFClause.cs

@@ -49,14 +49,7 @@ public CNFClause(Sentence sentence)
         public IReadOnlySet<Literal> Literals => literals;
 
         /// <summary>
-        /// <para>
         /// Gets a value indicating whether this is a Horn clause - that is, whether at most one of its literals is positive.
-        /// </para>
-        /// <para>
-        /// No caching here, but the class is immutable so recalculating every time is wasted effort, strictly speaking.
-        /// Various things we could do, but for the moment I'm erring on the side of doing nothing, on the grounds that these
-        /// properties are unlikely to be on the "hot" path of any given applicaiton.
-        /// </para>
         /// </summary>
         public bool IsHornClause => Literals.Count(l => l.IsPositive) <= 1;
 
@@ -65,7 +58,7 @@ public CNFClause(Sentence sentence)
         /// Gets a value indicating whether this is a definite clause - that is, whether exactly one of its literals is positive.
         /// </para>
         /// <para>
-        /// NB: this means that the clause can be written in the form L₁ ∧ L₂ ∧ .. ∧ Lₙ ⇒ L, where none of the literals is negated
+        /// NB: this means that the clause can be written in the form L₁ ∧ L₂ ∧ .. ∧ Lₙ ⇒ L (where none of the literals is negated)
         /// - or is simply a single non-negated literal.
         /// </para>
         /// </summary>

src/SCFirstOrderLogic/SentenceCreation/OperableSentenceFactory.cs

@@ -121,8 +121,7 @@ public static OperableSentence AreEqual(OperableTerm left, OperableTerm right) =
         /// </summary>
         /// <param name="identifier">The identifier of the variable.</param>>
         /// <returns>A new <see cref="OperableVariableDeclaration"/> instance.</returns>
-        public static OperableVariableDeclaration Var(object identifier) =>
-            new OperableVariableDeclaration(identifier);
+        public static OperableVariableDeclaration Var(object identifier) => new(identifier);
 
         #region VariableDeclarations
 

src/SCFirstOrderLogic/SentenceCreation/SentenceFactory.cs

@@ -154,8 +154,7 @@ public static Sentence AreEqual(Term left, Term right) =>
         /// </summary>
         /// <param name="identifier">The identifier of the variable.</param>>
         /// <returns>A new <see cref="VariableDeclaration"/> instance.</returns>
-        public static VariableDeclaration Var(object identifier) =>
-            new VariableDeclaration(identifier);
+        public static VariableDeclaration Var(object identifier) => new(identifier);
 
         #region VariableDeclarations
 

src/SCFirstOrderLogic/SentenceCreation/SentenceParser.cs

@@ -96,7 +96,7 @@ private static FirstOrderLogicParser MakeParser(string input)
 
         private class ThrowingErrorListener : BaseErrorListener
         {
-            public static ThrowingErrorListener Instance = new ThrowingErrorListener();
+            public static ThrowingErrorListener Instance = new();
 
             public override void SyntaxError(TextWriter output, IRecognizer recognizer, IToken offendingSymbol, int line, int charPositionInLine, string msg, RecognitionException e)
             {

src/SCFirstOrderLogic/SentenceManipulation/StandardisationExtensions.cs

@@ -5,7 +5,10 @@
 // TODO-BREAKING-V6: awkwardness - don't like the need for that explanatory comment about the type
 // of the new identifiers. Perhaps look at adding this at the same time as moving/renaming
 // the normalisation identifiers, to make it clear that they are only one way of representing
-// thee concepts, and are specific to our conversion classes.
+// the concepts, and are specific to our conversion classes.
+// And/or (don't like this, but..) could introduce StandardisedLiteral, StandardisedPredicate,
+// StandardisedTerm, StandardisedFunction, StandardisedVariable, etc - in which variable identifiers
+// are StandardisedVariableIdentifier, not object..
 #if false
 namespace SCFirstOrderLogic.SentenceManipulation
 {