doc tweaks

Author: sdcondon

src/SCFirstOrderLogic.Tests/FormulaFormatting/FormulaFormatterTests.cs

@@ -9,24 +9,26 @@ public static class FormulaFormatterTests
     public static Test FormatBehaviour => TestThat
         .GivenEachOf<FormatTestCase>(() =>
         [
-            new(Formula: "P(C())",            Expected: "P(C())"),
-            new(Formula: "P() & Q() & R()",   Expected: "P() ∧ Q() ∧ R()"),
+            new(Formula: "P(C())", Expected: "P(C())"),
+            new(Formula: "P() & Q() & R()", Expected: "P() ∧ Q() ∧ R()"),
             new(Formula: "[P() | Q()] & R()", Expected: "[P() ∨ Q()] ∧ R()"),
             new(Formula: "P() | [Q() & R()]", Expected: "P() ∨ [Q() ∧ R()]"),
-            new(Formula: "![P() | Q()]",      Expected: "¬[P() ∨ Q()]"),
-            new(Formula: "![P()]",            Expected: "¬P()"),
+            new(Formula: "![P() | Q()]", Expected: "¬[P() ∨ Q()]"),
+            new(Formula: "![P()]", Expected: "¬P()"),
 
             //∃∀
-            new(Formula: "∃ x, P(x)",        Expected: "∃ x, P(x)"),
+            new(Formula: "∃ x, P(x)", Expected: "∃ x, P(x)"),
             new(Formula: "∃ x, P(x) | Q(x)", Expected: "∃ x, P(x) ∨ Q(x)"),
             new(Formula: "∃ x, P(x) => Q(x)", Expected: "∃ x, P(x) ⇒ Q(x)"),
 
-            new(Formula: "∃ x, ∀ y, P(x, y)",        Expected: "∃ x, ∀ y, P(x, y)"),
+            new(Formula: "∃ x, ∀ y, P(x, y)", Expected: "∃ x, ∀ y, P(x, y)"),
 
             new(Formula: "∀ x, P(x) => Q(x) => R(x)", Expected: "∀ x, [P(x) ⇒ Q(x)] ⇒ R(x)"),
 
             new(Formula: "∀ x, ∀ y, P(x, y)", Expected: "∀ x, y, P(x, y)"),
             new(Formula: "∃ x, ∃ y, P(x, y)", Expected: "∃ x, y, P(x, y)"),
+
+            new(Formula: "∀ x, [∀ y, Animal(y) ⇒ Loves(x, y)] ⇒ [∃ y, Loves(y, x)]", Expected: "∀ x, [∀ y, Animal(y) ⇒ Loves(x, y)] ⇒ [∃ y, Loves(y, x)]")
         ])
         .When(tc => new FormulaFormatter().Format(FormulaParser.Default.Parse(tc.Formula)))
         .ThenReturns()

src/SCFirstOrderLogic/CNFClause.cs

@@ -10,8 +10,8 @@ namespace SCFirstOrderLogic;
 
 /// <summary>
 /// <para>
-/// Streamlined representation of an individual clause (i.e. a disjunction of <see cref="Literal"/>s) of a first-order logic formula in conjunctive normal form.
-/// Consists of a set of <see cref="Literal"/>s.
+/// Streamlined representation of an individual clause of a first-order logic formula in conjunctive normal form (CNF).
+/// Consists of a <see cref="IReadOnlySet{T}"/> set of <see cref="Literal"/>s.
 /// </para>
 /// <para>
 /// Note that this type is NOT a subtype of <see cref="Formula"/>. To represent a clause as a <see cref="Formula"/>, 

src/SCFirstOrderLogic/CNFFormula.cs

@@ -10,8 +10,8 @@ namespace SCFirstOrderLogic;
 
 /// <summary>
 /// <para>
-/// Streamlined representation of a <see cref="Formula"/> in conjunctive normal form (CNF).
-/// Consists of a set of <see cref="CNFClause"/>s.
+/// Streamlined representation of a first-order logic formula in conjunctive normal form (CNF).
+/// Consists of a <see cref="IReadOnlySet{T}"/> of <see cref="CNFClause"/>s.
 /// </para>
 /// <para>
 /// Note that this type is NOT a subtype of <see cref="Formula"/>. To represent CNF as a <see cref="Formula"/>, 
@@ -39,7 +39,13 @@ public CNFFormula(IEnumerable<CNFClause> clauses)
     }
 
     /// <summary>
+    /// <para>
     /// Initialises a new instance of the <see cref="CNFFormula"/> class from a <see cref="Formula"/> that is a conjunction of disjunctions of literals (a literal being a predicate or a negated predicate).
+    /// </para>
+    /// <para>
+    /// An <see cref="ArgumentException"/> will be thrown if the provided formula is not a conjunction of disjunctions of literals.
+    /// In other words, conversion to CNF is NOT carried out by this constructor.
+    /// </para>
     /// </summary>
     /// <param name="cnfFormula">
     /// The formula, in CNF but represented as a <see cref="Formula"/>. An <see cref="ArgumentException"/> will be thrown if it is not a conjunction of disjunctions of literals.

src/SCFirstOrderLogic/FormulaFormatting/FormulaFormatter.cs

@@ -10,7 +10,8 @@ namespace SCFirstOrderLogic.FormulaFormatting;
 
 /// <summary>
 /// This class provides functionality for rendering <see cref="Formula"/> instances (and <see cref="CNFFormula"/> instances) in the standard first-order logic syntax.
-/// Using a single <see cref="FormulaFormatter"/> instance allows for unique (and customisable) labelling of standardised variables and Skolem functions for all formulas formatted with the instance.
+/// Using a single <see cref="FormulaFormatter"/> instance allows for unique (and customisable) labelling of identifiers (e.g. standardised variables and Skolem functions)
+/// for all formulas formatted with the instance.
 /// </summary>
 public class FormulaFormatter
 {

src/SCFirstOrderLogic/FormulaFormatting/ILabeller.cs

@@ -5,7 +5,7 @@
 namespace SCFirstOrderLogic.FormulaFormatting;
 
 /// <summary>
-/// Interface for types capable of creating labels for identifiers that are unique (within a specified scope).
+/// Interface for types capable of creating labels for identifiers that are unique within a specified scope.
 /// </summary>
 public interface ILabeller
 {

src/SCFirstOrderLogic/_PackageFiles/SCFirstOrderLogic.md

@@ -3,10 +3,11 @@
 The SCFirstOrderLogic NuGet package contains basic but fully functional and documented [first-order logic](https://en.wikipedia.org/wiki/First-order_logic) implementations for .NET.
 Included are:
 
-* Implementations of both raw and CNF formula representation. 
+* A tree model for formulas.
+* A streamlined model for formulas in conjunctive normal form - a set of clauses rather than a tree.
 * Multiple ways of instantiating raw formulas, 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) formulas to be provided as lambda expressions.
-* Formula manipulation logic - base classes for formula visitors and transformations, as well as some implementations - e.g. normalisation, variable substitutions and basic unification logic.
-* Formula formatting logic that allows for (customisable) unique labelling of standardised variables and Skolem functions across a set of formulas.
+* Formula manipulation logic - base classes for formula visitors and transformations, as well as some fundamental implementations - normalisation, variable substitutions and basic unification logic.
+* Formula formatting logic that allows for (customisable) unique labelling of identifiers (e.g. standardised variables and Skolem functions) across a set of formulas.
 * Index structures for terms and clauses, with node abstractions to allow for consumer-provided backing stores. Specifically, we have discrimination tree, path tree and feature vector index implementations.
 
 Accompanying the core SCFirstOrderLogic package are three supporting packages: