# Can we find validity proofs by means of rules of inference with FindEquationalProof?

Can we find proofs such as:

Using FindEquationalProof? My guess is "yes" but I don't know what would be the "axioms" here nor how would we write this in Mathematica.

• Please take a look at Implementation of Common Axiom Systems and Proof Generation. Commented Feb 14 at 12:55
• I would do something like this as per the documentation pastebin.com/SYUQFEcZ. Unfortunately, I've had it running for 20 mins and it still hasn't finished running. Commented Feb 14 at 23:55
• What axioms do you want? Commented Mar 1 at 4:50
• @ShyPerson The rules of inference. I want it to apply rules of inference, don't know if this is possible though. Commented Mar 1 at 14:54

Here you go. The definition of Boolean Logic comes directly from the documentation of FindEquationalProof:

booleanLogic =
{ForAll[{a, b}, and[a, b] == and[b, a]],
ForAll[{a, b}, or[a, b] == or[b, a]],
ForAll[{a, b}, and[a, or[b, not[b]]] == a],
ForAll[{a, b}, or[a, and[b, not[b]]] == a],
ForAll[{a, b, c}, and[a, or[b, c]] == or[and[a, b], and[a, c]]],
ForAll[{a, b, c}, or[a, and[b, c]] == and[or[a, b], or[a, c]]]}
implicationDefinition = {ForAll[{a, b}, implies[a, b] == or[not[a], b]]}
premises = {implies[not[a], and[c, d]], implies[a, b], not[b]}
FindEquationalProof[c, Union[booleanLogic, implicationDefinition, premises]]


As to the original question of whether traditional rules of inference can be used in this part of Mathematica, the answer is no, because these are not equational theories, while the prover behind FindEquationalProof is an equational prover. More specifically, while the traditional inference rules are perfectly sound in the usual forward direction, a number of them are not correct in the reverse direction. For example, modus ponens is correct in the forward direction, but definitely not in the reverse direction. To be used in an equational prover, the rules have to be biconditional in order to be equations. So if you look at the Boolean logic axioms in my original solution, you will see they are all biconditional.

• @RedBanana: Glad you liked it. Please give a link to the rules of inference you want, and I'll see what I can do. Remember, the prover in Mathematica is just an equational prover, so everything has to be specified. It doesn't know the rules of inference innately. Commented Mar 10 at 5:47
• @RedBanana: Or did you just want me to do an ad hoc version where I use the rules of inference in your example? The other thing to bear in mind is that the proofs generated by an equational prover probably can't be expected to look as nice or as short as those in a natural deduction proof. Commented Mar 11 at 3:41
• I want to see if it's possible to make it prove that with the following rules of inference for propositional calculus. Do you think it's possible? Commented Mar 11 at 6:07
• This is really interesting, I know next to nothing about logic. I just finished a "baby logic" course and wanted to try Mathematica theorem proving for fun. I got curious about the following: Can we prove the same with both equational proofs and rules of inference? Commented Mar 11 at 21:52
• @RedBanana: Glad to hear of your interest in logic. I find it never gets old. As for your question, the rules of inference you cited are only for propositional logic, while equational proofs are a subset of first order logic, which is more powerful. So you can prove more in equational logic. Commented Mar 13 at 3:18