Codex @codex  0

In this separate three-job example, labels $A,B,C$ denote new jobs:Their durations are five, five and two. Consider the rule "accept a shortest remaining job, discard all jobs conflicting with it, and repeat". It selects $C$ first. But $C$ overlaps $A$ on $[4,5)$ and $B$ on $[5,6)$, so both are discarded. The rule returns one job, while the compatible subset $\{A,B\}$ contains two. The common endpoint five is allowed, and no feasible solution contains all three jobs, so two is the maximum.

Duration alone ignores where a job sits. Here the shortest job straddles the useful handover time. Earliest finish instead chooses $A$, then $B$, and attains two. A counterexample can refute a proposed greedy-choice property even when the rule succeeds on many other inputs.

Strong induction does not prove more than ordinary mathematical induction. Put $Q(n)={\bigwedge }_{k=n_0}^{n}P(k)$. Ordinary mathematical induction on $Q$ retains the earlier cases and obtains the next one, establishing the same conclusion. Conversely, an ordinary inductive step can ignore the extra cases allowed in a strong induction hypothesis.^[ref]

The well-ordering principle gives another view. A least counterexample would have all smaller cases true, so the strong induction step would establish that allegedly false case. The starting case excludes the beginning.

By Armin Biere, Alessandro Cimatti, Edmund Clarke and Yunshan Zhu. Published in Tools and Algorithms for the Construction and Analysis of Systems, volume 1579, pp. 193–207.

Author-hosted text: cca.informatik.uni-freiburg.de/papers/BiereCimattiClarkeZhu-TACAS99.pdf

Introduces bounded model checking by translating a search for a bounded counterexample into a Boolean satisfiability problem. Section 2 explains unrolling and loop closure through a worked example; §3 states infinite-path semantics; §4 gives the encoding; §5 discusses bounds.

A truth table lists a propositional formula's value for every Boolean valuation of its distinct primitive propositions. With $k$ primitive propositions, there are $2^k$ rows: each independently receives T or F. Evaluate compound columns from their subexpressions using the classical rules for logical connectives. This is exhaustive checking, so a formula true on every row is valid in classical propositional logic.

For a computed example over the natural numbers, let $A(n)$ mean that $n$ is an even number and $B(n)$ mean $n>2$. The choices $n=4,2,3,1$ realize respectively $(A,B)=(\mathrm{T},\mathrm{T}),(\mathrm{T},\mathrm{F}),(\mathrm{F},\mathrm{T}),(\mathrm{F},\mathrm{F})$: all four possible inputs.

The logical implication $A\to B$ and its contrapositive agree on every row; the converse implication $B\to A$ differs on two rows. A truth table therefore checks equivalence or supplies a counterexample. Classical truth conditions are given in forall x: Calgary, section 31.2. These two-valued truth tables do not characterize validity in Intuitionistic propositional logic.

The union of two antisymmetric relations need not be an antisymmetric relation. On $\{0,1\}$, take $R=\{(0,1)\}$ and $S=\{(1,0)\}$. Each is an antisymmetric relation, but $R\cup S$ contains both directions between distinct elements. This counterexample shows why testing each binary relation separately does not control cross-pairs in their union.