Note: These notes are a mixture of lecture material, textbook material and private research. All credit to the University of Melbourne.

Matt’s Patchy Notes.

Why study logic and discrete maths?

Logic and discrete mathematics form the foundation of computer science. They are the enabler for computation.

Many tools based on propositional logic e.g. Constraint solver

Finite-state automata are already sitting underneath lots of algorithms we already know and use.

What we are studying is not new, but we are constantly finding new applications.

Trying to strip away unneccessary detail of computational devices and learn the

Logic is a way of reasoning. Given premises and reach a conclusion.

Logic is the math of language.

By converting sentences into mathematical formulas we can reach conclusions.

The point of deductive logic is truth preservation.

Broad topics:

Logic/Discrete Maths
Automatas/Computability

Formal Languages

Just a set of strings.

Regular <-> finite automata

Context-free <-> pushdown automata

The sort of things we can do are only possible because of really good theories that people have come up with e.g. compilers, parsers. Theory and practice are very tightly intertwined in computer science and it is a symbiotic relationship.

Example

Propositional logic gives us a way of writing down statements and manipulating them mechanically

Haskell

Very good at symbolic reasoning. Good at solving particular programs.

Scanner is a “deterministic finite state machine (DFA)”

Propositional Logic

People like to model their problems in propositional logic. Use boolean logic and send it to a sat-solver (maniupulate boolean logic very fast).

Every sentence has a truth value.

All problems here are solvable and decidable (not the case with predicate logic).

Boole had an algebraic view of logic.

Negation
Conjunction / AND
Disjunction / OR
Implication / If-then
Biimplication / If-and-only-if
Exclusive OR / XOR

In terms of binding tightness:

Negation > conjunction/disjunction > XOR > imp/biimp

A	B	Neg A	A AND B	A OR B	A => B	A <=> B	A XOR B
0	0	1	0	0	1	1	0
0	1	1	0	1	1	0	1
1	0	0	0	1	0	0	1
1	1	0	1	1	1	1	0

A and B stand for arbitrary, complicated, well-formed formulas

A => B - the only way we can deny it, is if we have A and not B. If A, then B. Not a causal relationship, doesn’t mean that A implies B.

A => B - has the same truth table as (NOT A) OR B

Conjunction is not a strict function in Haskell. Doesn’t insist on evaluating all arguments.

When reasoning about programs, often need 3-valued logic. 2 truth values and one that is undefined.

Logic Concepts

A propositional formula is valid if no truth assignment makes it false.

Valid formula will have truth table of all true.

It is unsatisfiable if no truth assignment makes it true. Otherwise it is satisfiable.

e.g. satisfiable -> possible to make it true

A valid propositional formula is a tautology.

An unsatisfiable propositional formula is a contradiction

Unsatisfiable formula will have truth table of all false.

valid3 :: (Bool -> Bool -> Bool -> Bool) -> Bool
valid3 f
  = and [f p q r | p <- b, q <- b, r <- b]
    where
      b = [False, True]

satisfiable3 :: (Bool -> Bool -> Bool -> Bool) -> Bool
satisfiable3 f
  = or [f p q r | p <- b, q <- b, r <- b]
    where
      b = [False, True]

Validitity is preserved by substitution of propositional letters and formulas.

A formula is unsastisfiable iff its negation is valid.

Substitution also preserves unsatisfiability.

Doesn’t always preserve satisfiability.

e.g. P is satisfiable, but subsituted for Q AND NOT Q it is not.

Truth Assigment - mapping of variables to values.

If a truth assignment makes a propositional formula true, then it is a model of the formula.

psi is a logical consequence of phi iff every model of phi is a model of psi as well.

Substitution preservers logical equivalence.

Interchange of equivalents. Replacing equals by equals yields equals. It preserves:

logical equivalence
logical consequence
validity
unsatisfiability
satisfiability (unlike substitution)

When using a sat-solver, we can send a formula to sat-solver that isn’t logically equivalent, but also preserves satisfiability.

Mechanised Reasoning

Mechanising deduction

Propositional logic is decidable.

Satsifiability is NP-complete, and was one of the first NP-complete questions to be explored.

Importatn problems in scheduling, network flow, routing, db management etc are tractable if and only if SAT is. Most computer scientists think that it is unlikely that there are decision procedures for SAT that perform much better than brute force.

Normal forms for propositional logic

Literal - is P or NOT P where P is a propositional letter
Conjunctive Normal Form - if it is a conjunction of disjunctions of literals (or a conjunction of “clauses”) e.g. (A OR NOT B) AND (B OR C OR D) AND A
Disjunctive Normal Form - disjunction of conjunctions of literals e.g. (NOT A AND NOT B) OR (NOT B AND C) OR (A AND NOT D)

Every propositional formula can be expressed in CNF as well as DNF.

Steps to convert to CNF/DNF

Eliminate XOR A XOR B === (A OR B) AND (NOT A OR NOT B)
Eliminate biimp A <=> B === (A => B) AND (B => A)
Eliminate imp A => B === NOT A OR B
Push NOT inward over AND/OR
Eliminate double negations
Use distributive laws

Normal form does not mean unique form.

In a normal form leads to a unique representation it is called canonical.

Binary Decision Diagrams (BDD)

Implement a BDD with hashing.

ROBDD - Reduced, ordered BDD

SAT solvers don’t use BDD as its expensive to get it into that form.

Translating into set notation is also called providing “clausal form”. This stresses the fact that the order in CNF doesn’t matter.

Empty clauses

The empty clause {} represents BOTTOM or false

Empty CNF formulas

The empty CNF formula represents TOP or true

Predicate Logic

Much more expressive than propositional logic.

Can translate most things in natural language to predicate logic.

Allows us to:

express statements that deal with infinite collections of objects
express relations, capturing transitive verbs and relative pronouns

Uses variables that range over collections of individuals, such as integers, graphs, people etc, as well as quantifiers.

Used to have propositional letters, now have predicates.

V - Universal quantifier

!E - Existential quantifier

Lambda functions - create functions without giving them names.

Lambda Haskell:

\x -> x^2 + 1

A term is a variable or a constant

Constants can be considered functions that take no arguments.

Term - individual, object Atom - assertion (false or true)

A literal is an atomic formula or it’s negation

Predicates start with upper case letter.

father(ron) is a term, denotes an object e.g. the father of Ron

Father(ron) is a formula, denotes a truth value e.g. Ron is a father

A variable in the scope of a quantifier is bound. If not bound, then free.

Word order is important:

“there is something which is not P” : !Ey NOT P(y)
“there is not something which is p” : NOT !Ey P(y)
“all S are not P” : Vx (S(x) => NOT P(x))
“not all S are P” : NOT Vx (S(x) => P(x))

The order of quantifiers is important.

$\forall$ x $\exists$ y != ! $\exists$ y $\forall$ x

Interpretations don’t talk about variables.

The truth of a closed formula should depend only on the given interpretation.