Logic & Reasoning

Variables that are true or false, joined by not, and, or, if-then, and iff. A truth table lists every world and evaluates the formula in each: what is always true, never true, or sometimes true.

Every formula can be rewritten as an and of or-clauses, or an or of and-terms. Read the form off the truth table, or rewrite with De Morgan and distribution; CNF is the shape a SAT solver takes.

Is there an assignment that makes every clause true? Propagate what the clauses force, guess only when nothing is forced, and back out of a dead branch: the search behind every modern solver.

Variables, domains, and constraints between them: colour a map, place queens. Assign one variable at a time, prune what each choice rules out, and undo when a domain runs dry.

Start from the facts and fire each rule whose premises are known, until the goal appears or nothing new follows. For Horn clauses that is linear, sound, and complete: the heart of a rule engine.

Add the goal's negation to the clauses and resolve clashing pairs until the empty clause appears. One rule, complete for propositional logic, and the engine beneath every theorem prover and Prolog.

Relations over objects, variables bound by for-all and there-exists, and truth decided by checking a formula against a model. Why swapping two quantifiers changes the answer, one lookup at a time.

Find the bindings that make two terms with variables identical, and the most general ones. Robinson's algorithm, pair by pair, with the occurs check that keeps the answer finite.

A program is facts and rules; a query is a goal to prove. Resolution picks the first goal, unification matches a clause, backtracking tries the rest: SLD resolution, Prolog's engine, step by step.