Proves both De Morgan's law and its negation

[CapacitorSet]

De Morgan's law states that !A & !B = !(A | B).

Using the demo on your website, I entered the facts A -> B and A as the Knowledge Base and asked it to prove De Morgan's law (though as a simple implication rather than as an equality), which it did successfully:

Step	Sentence	Action
0	(A -> B)	initial expression
1	(!A | B)	eliminate implication
2	A	initial expression
3	(!A | B)	knowledge base clause from 1
4	A	knowledge base clause from 2
5	!A	assume for a contradiction
13	false	resolve of 4 and 5
/	/	By assuming the negation of the query, we are able to derive a contradiction. Therefore, the knowledge base combined with the negation of the query is unsatisfiable, so the query follows from the axioms of the knowledge base.
	(!A & !B) -> !(A | B)	by resolutional inference

However, I got the same proof when asking it to prove (!A & !B) -> (A | B), which is the negated version of the first and should therefore be unprovable.

[RyanMarcus]

With a knowledge base of:

(1) A
(2) A -> B

... and a query of (!A & !B) -> !(A | B), we have:

(3) A is true, from KB 1
(4) (!A & !B) is false, since A is true (by 3)
(5) (!A & !B) -> !(A | B) is true, since F -> alpha is always true

So the statement (!A & !B) -> !(A | B) is (vacuously) true, given the knowledge base.

The same argument is true for (!A & !B) -> (A | B). Since (!A & !B) is false given the knowledge base, any implication with a false thing on the left-hand side is true.

To prove De Morgan's law, use a knowledge base of "!A" and "!B". Then, the claim (!A & !B) -> !(A | B) will be proven, but the claim (!A & !B) -> (A | B) will not be proven.

It took me a while to keep it all straight in my head -- sorry for the confusion. :) One thing that is interesting is that Vulcan will declare the statement (!A & !B) <-> !(A | B) false given no knowledge base. I'm honestly not sure if this is correct or incorrect behavior. On the one hand, the statement is a tautology (always true), but on the other hand, no statements are derivable from an empty knowledge base... this might be one for the philosophers.