You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
That can be done in two ways (one simple, one not so simple)
Making some assumptions and counting state, analysing the clause often before making a move
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
The text was updated successfully, but these errors were encountered:
That can be done in two ways (one simple, one not so simple)
Regardless of what is chosen, there are some things that need to be implemented nonetheless
reduce
there needs to be aconsider_reduce_choices
function which returns a set of terms that can be acted on, saying what operation can be performedreduce
function then needs to build priorities according to the resolution rulesDerivations 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
The text was updated successfully, but these errors were encountered: