I need a function which gives possible solutions for a variable that make it true. The function would be something along the line of this.
In:= Function[a \[Implies](b \[Implies] c) , c]
Out:= c -> a
It would give this because replacing c with a in a \[Implies](b \[Implies] c) would make it a tautology, and is the shortest rout to do so.
If there are multiple equally short solutions, it would give a list of solutions.
The main attribute of this function would be to expand a variable into longer strings. For example;
In:= Function[a\[Implies]((b\[Implies]c)\[Implies](b\[Implies]d)) , a]
Out:= a -> b\[Implies](c\[Implies]d)
This would be the shortest rout to turning the function into a tautology.
Does such a function exist? It's not on Wolfram Research's list of boolean functions.
I'm not sure how I would go about defining a function like this. The main problem is getting a variable to expand a single variable into longer strings.