SCFirstOrderLogic

Basic but fully functional and documented first-order logic implementations. Heavily influenced by "Artificial Intelligence: A Modern Approach" (Russell & Norvig). Intended first and foremost to assist with learning and experimentation, but does include extension points (and async support) so that it is at least conceivable that it could be (extended to be) useful in a production scenario. Includes:

• Implementations of both raw and CNF sentence representation. Multiple ways of instantiating raw sentences, including 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 versions of their respective algorithms, do 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. As such, care has also been taken to include good type and member documentation, as well as Source Link to allow for debugging - and explanatory inline comments in the source code where appropriate.

Full documentation can be found via the FlUnit repository readme.