AUTOMATED THEOREM PROVING PROPOSITIONAL LOGIC (AKA PREDICATE LOGIC) P Q P^Q PvQ ~P T T T T F T F F T F F T F T T F F F F T if (x==7 and y==5) 100 IF X=7 GOTO 200 150 GOTO 400 200 IF Y=5 GOTO 300 250 GOTO 400 300 PRINT "YAY" 350 GOTO 500 400 PRINT "BOO" 500 END So, suppose you have a set of logical statements. How can you tell if they logically entail the conclusion? (PvQ) ~P Q (PvQ)^~P Q TTT FF T TTF FF F FTT TT T FFF FT F The final column on the left does not have to match the final column on the right. However, if T on the left never corresponds to an F on the right, then the left side "entails" the right side. (If the left side is true, the right side must also be true.) So, generating truth tables can be considered a form of automated theorem proving. But it's sucky. This also demonstrates that predicate logic is complete. "Soundness" and "Completeness". A logical system is "sound" if the rules are consistent. You cannot prove a false thing under the system. A logical system is "complete" if every true thing can be proven within the system. x^n+y^n = z^n, x,y,z, integers, n > 2, x, y, z > 0 3^2 + 4^2 = 5^2, but are there situations where x^3 + y^3 = z^3? 6-->3-->10-->5-->16-->8-->4-->2-->1 Collatz conjecture: you will always get to 1 eventually. Imagine True = 1 False = 0. (I've tried True = 1 and False = -1) ~P = 1-P (P^Q) = PQ (PvQ) = P+Q - PQ P^2 = P When I've tried T=1 and F=-1, I did this specifically so that P^2 = 1. In this model, ~P = -P (P^Q) = -0.5 + 0.5P + 0.5Q + 0.5PQ (PvQ) = 0.5 + 0.5P + 0.5Q - 0.5PQ (PvQ) = 1+P-PQ ~P = 1-P (PvQ)^(~P) =(P+Q-PQ)(1-P) = (P+Q-PQ-P^2-PQ+P^2Q) = (P+Q-PQ-P-PQ+PQ) = Q-PQ I want to show that (PvQ) and ~P logically entail Q. Is I "and" my premises with the negation of the conclusion. (Q-PQ)(1-Q) = Q -PQ -Q +PQ = 0. If I get zero, this means that my premises are inconsistent with the negation of the conclusion. It means there is no way the negation of the conclusion can be true, so the conclusion must be. If I get zero, the conclusion follows from the premises. If I get ANYTHING else, the result is not proven. Given P, can I conclude PvQ P = P PvQ = P+Q-PQ ~(PvQ) = 1-P-Q+PQ P(1-P-Q+PQ) = P-P-PQ+PQ = 0, so conclusion must be true. To do this as a computer program, remember that P^2 = P, so every term contains no more one instance of each variable. So, a term can be expressed as an array or a list or whatever of booleans, indicating which variable is in that term. And a coefficient. And a logical expression consists of an array or list or whatever of these terms. If you "and" or multiply two terms, all you do is "or" the booleans, if a variable is in either term, it's in the product, and just multiply the coefficients. If you multiply two expressions, you (double loop) multiply each term in the first with each term in the second, and add them up. You will have to combine like terms. If you have 4[T,F,T] and 2[T,F,T] then they will have to be combined into 6[T,F,T]. There are never any fractions in this process. (P^~Q) Q ==> 1[F,T] ~Q ==> 1[F,F] -1[F,T] (1-Q) P ==> 1[T,F] 1[T,F] -1[T,T] P-PQ Q = 1[F,T] ((P^~Q)^Q) 1[T,T] -1 [T,T] = 0[T,T] 0 if (x==7 and y==5) 100 IF X=7 GOTO 200 150 GOTO 400 200 IF Y=5 GOTO 300 250 GOTO 400 300 PRINT "YAY" 350 GOTO 500 400 PRINT "BOO" 500 END 100 LET P = 0 110 IF X=7 THEN LET P=1 120 LET Q = 0 130 IF Y=5 THEN LET Q=1 140 IF (P*Q=1) THEN GOTO 400 150 PRINT "BOO" 160 GOTO 500 400 PRINT "YAY" 500 END Short-circuit boolean: In most modern programming languages if (P && Q) If P works out to be false, Q is not even evaluated at all because P && Q is now known to be false, no matter what Q is. Similarly, Q is not evaluated in (P || Q) if P happens to work out to true. There's no need to, since P || Q is true. if (i < n && A[i]%2==0) countevens++; If the array size is n, and that's why I'm testing for it, then this prevents an out of bounds error. if (A[i]%2==0 && i < n) countevens++; This no longer works because I might go out of bounds on A[i] (x==0)?a:b In C/C++, if the first thing is true, the second thing is evaluated and returned. if the first thing is false, the third thing is evaluated and returned. if (x==0) return 17 else return -5 return (x==0)?17:-5