This function is essentially a dry-run of the reduce function. It needs some of the functions described in #8 to work properly (and not be too bloated) and returns a set of possible actions, ordered by their appeal.

Then either the user (or an engulfing algorithm can pick whichever it thinks is best and execute it

Terms and Clauses are kinda the same thing just with different operators. So they should share some code. Could use an enum or a common "Logic" type or something like that

It should be possible to call println!("{:?}", my_term) and actually get the (example) output: { A, ¬B, C }. Should probably look into how to do that 😅

Coming out of #9 is a set of possible operations on a clause which are ordered in their appeal to an algorithm (or certain parameters maybe). After this the API needs a function to take one of these operation structs and execute the reduction on a clause

That can be done in two ways (one simple, one not so simple)

1. Making some assumptions and counting state, analysing the clause often before making a move
2. Implement a trial system and backtracking in case a branch didn't work out

Regardless of what is chosen, there are some things that need to be implemented nonetheless

• Instead of calling reduce there needs to be a consider_reduce_choices function which returns a set of terms that can be acted on, saying what operation can be performed
• The reduce function then needs to build priorities according to the resolution rules
• Record every action taken in the clause history (implement a queue?)
• Add a results struct into the clause that can be slowly filled with data as it trickles in

Derivations are simple and can immediately lead to a field in the result struct.

Merges are a bit more complicated because they might need to be performed in a specific order { A, B }, { !A, D }, { A, B! } for example.

To be continued

Something to think about when redesigning some of the internal structures talked about in #4... 🤷‍♀️

Sometimes a clause is solvable but it's result isn't one set of interpretations for it's set of symbols. Therefore lrs needs to be able to handle "fuzzy" (what is the technically correct term for this?) results.

The clause { A, B } has the results:

This can either be done by

• Letting the final resolve function return a list of possible interpretations
• Changing the "LResult" struct (Should this be named Interpretation instead?) to handle these fuzzy-cases

Instead of assuming CNF we should be able to take any logical equation and transform it into a normal_form of the users liking

lrs can do a few things already but especially terms need more awareness of what's inside them. So there need to be a few utility functions that handle this. They don't need to be super fast (at least not for now) but need to provide easily callable functionality.

• Find offending terms in a term ({ A, ¬A } which will start a branch reduce run)
• Count occurrences of symbols in a clause ({ A, ¬B }, { A, C } should result in A: 2, ¬B: 1, C: 1)
• Recognise "fuzzy results" ( { A, B } works with A=1, B=1 and A=1, B=0 and A=0, B=1 See #10)

The lrs crate is still pretty simple but there are already some stuff we can unit test

• Create terms with symbols
• Join terms together
• Remove symbols from terms

When feature complete we can also test complete clause resolutions

It should be possible to give lrs any (propositional – let's talk about first order later) logical clause that it can then transform to CNF, DNF and NNF as the user requests or an algorithm sees fit.