Irving Copi & Carl Cohen, Introduction to Logic, 10th edition (Prentice Hall, 1998).

• Categorical Logic: Three chapters in Copi address categorical logic, one on categorical propositions, one on syllogisms, and one on translation. Venn diagrams are not introduced until the second of these chapters, while the first focuses on immediate inferences and the square of opposition. A chapter focusing on ordinary language arguments rounds out this section.
• Propositional Logic (unquantified logic): Copi's treatment of propositional logic begins with a 50-page chapter explaining connectives and equivalence (including de Morgan's theorems). A briefer chapter on proofs follows, which develops the 9 inference rules and 10 rules of replacement of the Copi proof system.
• Predicate Logic (quantified logic, first order logic, elementary logic): A single chapter introduces predicate logic and extends the proof techniques to them. The introduction of the ideas of predicate logic and quantification is good, but there is no discussion of relational predicates.
   

Some different types of logics that are of importance to computer science
* Propositional/Boolean logic: the design of combinatorial electronic circuits; program control
* Predicate logic: formal specification, prolog programming language
* Higher-order logic (e.g., second order logic): formal verification of hardware
* Sequential/temporal logic: design of computer memory; program concurrency
* Intensional logic: natural language processing; human-computer interaction

Propositional Logic 

A proposition is a statement that can be true or false. Propositional logic uses true statements to form or prove other true statements.

There are two parts to propositional logic:

Representation (syntax): How to represent a proposition.
Reasoning (algorithm): How to create or prove new propositions.

A simple statement (atomic proposition) is one that does not contain any other statement as a part. We will use the lower-case letters, p, q, r, ..., as symbols for simple statements.

A compound statement (compound proposition) is one with two or more simple statements as parts or what we will call components. A component of a compound is any whole statement that is part of a larger statement; components may themselves be compounds.

An operator (or connective) joins simple statements into compounds, and joins compounds into larger compounds. We will use the symbols, , · , , and to designate the sentential connectives. They are called sentential connectives because they join sentences (or what we are calling statements). The symbol, ~, is the only operator that is not a connective; it affects single statements only, and does not join statements into compounds.

The symbols for statements and for operators comprise our notation or symbolic language. Parentheses serve as punctuation.

Simple statements

Compounds and connectives

p q	"either p is true, or q is true, or both"	disjunction
p · q	"both p and q are true"	conjunction
p q	"if p is true, then q is true"	implication
p q	"p and q are either both true or both false"	equivalence

Implication statements (p q) are sometimes called conditionals, and equivalence statements (p q) are sometimes called biconditionals.

Representation:

A proposition is defined as:
1. A propositional symbol: p (propositions will always be lowercase)
2. The negation of a proposition: !p (traditionally a '¬' symbol)
3. The disjunction of two propositions: p+q (traditionally a 'v' symbol)
4. The conjunction of two propositions: p*q (traditionally a '^' symbol)
5. An implication: p=>q
6. A logical equivalence: p<=>q
7. An ordering operation: (p)
8. T (true)
9. F (false)
• Converse of "If p, q" is "If q, p".
• Inverse of "If p, q" is "If not p, not q".
• Contrapositive of "If p, q" is "If not q, not p".

The order of operations is !, *, +, =>, <=>

This definition can be decribed by the following unambiguous BNF grammar:


Sentence -> EquivalenceSentence
EquivalenceSentence -> ImplicationSentence <=> EquivalenceSentence | ImplicationSentence
ImplicationSentence -> ConjunctiveSentence => ImplicationSentence | ConjunctiveSentence
ConjunctiveSentence -> DisjunctiveSentence + ConjunctiveSentence | DisjunctiveSentence
DisjunctiveSentence -> NegateSentence * DisjunctiveSentence | NegateSentence
NegateSentence -> !NegateSentence | GroupingSentence
GroupingSentence -> (Sentence) | AtomicSentence
AtomicSentence -> T | F | p | q | r | ...


The value of a proposition can be found by making a truth table from its components.

Example: (p*q)+r

	
		p	q	r	p*q	(p*q)+r
		0	0	0	0	0
		0	0	1	0	1
		0	1	0	0	0
		0	1	1	0	1
		1	0	0	0	0
		1	0	1	0	1
		1	1	0	1	1
		1	1	1	1	1

Properties of Propositional Operators:

	+ and * are communitive:
		p+q <==> p+p
		p*q <==> p*p
	+ and * are associative:
		(p+q)+r <==> p+(q+r)
		(p*q)*r <==> p*(q*r)
	+ is distributable over *:
		p+(q*r) <==> (p+q)*(p+r)
	* is distributable over +:
		p*(q+r) <==> (p*q)+(p*r)
	DeMorgan's Theorem:
		!(p+q) <==> !p * !q
		!(p*q) <==> !p + !q
	Complementation:
		!(!p) <==> p

Symantics and Definitions:

Interpretation

An interpretation can be described as one line of the truth table.
An interpretation can also be described as a mapping named 'G' that
takes a set of propositions named 'P' and returns T or F.
Example: (p*q)+r is true for interpretation G(pqr)=011

Valid

A proposition is valid if it is true for any interpretation G.
Example: p+!p is Valid (p or not p)

Satisfiable

A proposition is satisfiable it is true for at least one interpretation G.
Example: p is satisfiable since p is true for G(p)=1

Unsatisfiable

A proposition is unsatisfiable if is false for all interpretations.
Example: p*!p is false for G(p)=0 and G(p)=1.

Literal

A propositional symbol or its negation. Expressed as L
Examples: p, !p

Clause

A disjunction of literals. Expressed as C
Example: p + !p + q, L1 + L2 + L3

Conjunctive Normal Form (CNF)

A conjunction of clauses. This is the basis of a rule set or knowledge base.
Example: (p+q+r)*(!p+q+r), C1*C2*C3

Mathematical Notation

    G:P => {T,F}
	    Interpretation G takes a set of propositions P and returns an element T or F.
    G |= P
	    P is true for interpretation G. 
	    '|=' is a single symbol known as a double turnstyle.
    G != P
	    P is not true for interpretation G.

Reasoning:

Theorem:

p is valid iff !p is unsatisfiable.
If there exists no interpretation for which !p is true, the p must be true for all interpretations.


This theorem is the basis of reasoning in propositional logic.

Rules of Inference:

A way to derived new propositions or simplify existing ones.

Modus Ponens

	If p=>q is true and p is true, then q must be true.
		
		p=>q		!p+q
		p			 p
	---			---
		q			 q

	If a drunk person swerves while driving and the person is drunk, then the car is swerving.
		

Modus Tolens

	If p=>q is true and q is false, then p must be false.

		p=>q		!p+q
	!q			!q
	---			---
	!p			!p

	If a drunk person swerves while driving and the car is not swerving, then the person is not drunk.
		

And-Elimination

	If p*q is true, the p is true and q is true
			
	p*q
	---
	 p
		

Or-Introduction

	If p is true, then p+q is true.

	 p
	---
	p+q
		

Double-Negation Elimination

	The negative of a negative is a positive.

	!!p
	---
	 p
		

Resolution

	Because b and !b cannot both be true, one of the other literals in
	a disjunction must be true. 

	a+b * !b+c		!a=>b * b=>c
	----------		-------------
	   a+c			     a=>c

	Resolution is the most powerful of the rules of inference since it allows
	us to create new clauses from what we know.
		

This is all we have to reason. Other forms are considered bad logic:

If p=>q is true and q is true, it does not necessarily mean that p is true.
((p=>q)*q) => p is not a Valid statement (although it is satisfiable)


If a drunk person swerves while driving and the car is swerving, then the person may or may not be drunk.

More on Resolution

The process of deriving new valid clauses from a CNF is called resolution.

Any two clauses in a valid CNF with one set of complementing literals can be disjoined together to create a new clause.

Within the new clause duplicate literals can combined to simplify it.

Example: C1*C2 <==> T

			C1: !a+b+c+d
			C2: a+b+c+e
			--------------------
			C3: b+b+c+c+d+e (by resolution)
			C3: b+c+d+e

			Thus C1*C2*C3 <==> T
        

Note that resolving two clauses with more than one set of complementing literels is not useful.

Example: C1*C2 <==> T,

			C1: a+b
			C2: !a+!b
			-------------------
			C3: a+!a
			C4: b+!b
        

Since (a+!a) is T regardless of the state of a, the CNF becomes C1*C2*T*T. Conjunction of T with a true statement does not add anything to the statement.

Proving Propositions using Resolution:

Recall that if a statement is unsatisfiable, then its negation must be valid.

If the clauses in a CNF can be resolved to an empty set {}, then the CNF is unsatisfiable.

Example: K:C1*C2

				C1: b
				C2: !b
				----------------
				C3: {}
			

An empty set is implicitly defined as false. Any statement P, made up of the disjunctions p1+p2+...+pn, can also be represented as P+F. The disjunction of F does not change the truth of P. If we resolve P+F and !P+F, we get F. Conjuncting F with the original statement C1*C2*F, shows that the statement is always false. This means that the negation of that statement is always true.

If a clause (C) is conjoined with a valid CNF (K) and the resulting CNF (K*C) is unsatisfiable, then C must be unsatisfiable and thus its inverse (!C) must be valid.

Proof: Given that K*!C is unsatisfiable.

				!(K*!C)		valid by definition
				!K+!!C		by DeMorgan
				!K+C		by double negation
				K=>C		If K is true then C is true.
			

Given any rule base K, and a negated conclusion !C we can prove that K implies C if and only if K and !C implies an empty statement {}. R=>C iff R*!C=>{}

Example: K:C1*C2*C3 C:r

				C1: p
				C2: p=>q
				C3: q=>r
				C4: !r
				----------------
				C5: !p+q    (C2)
				C6: !q+r    (C3)
				C7: !p+r    (C5,C6)
				C8: r       (C1,C7)
				C9: F,{}    (C4,C8)       
			

Since !C results in a contradiction, C must always be true.