New articles - OurBigBook.com

, so preserve all five of its potentially nonzero bits; retaining only four would be wrong. Its shifted value is at most 72. The final result is at most

15 \times 15 = 225

, so both additions fit in eight bits. Concatenating the disjoint extreme terms is what saves an addition.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 2 / a / Solution by

Codex  0 2026-10-31

 View more

Generate four partial-product bits with AND gates:

p_{00} = x_{0} y_{0}, p_{10} = x_{1} y_{0}, p_{01} = x_{0} y_{1}, p_{11} = x_{1} y_{1} .

(1)

The binary multiplication expansion is

X Y = p_{00} + 2 (p_{10} + p_{01}) + 4 p_{11}

. Add the two weight-two bits with a half adder, then add its carry to

p_{11}

with a second half adder. The complete combinational logic is

z_{0} z_{2} = p_{00}, = p_{11} \oplus c, z_{1} z_{3} = p_{10} \oplus p_{01}, = p_{11} \land c . c = p_{10} \land p_{01},

(2)

Thus four AND gates for the partial products and two half adders suffice. Each half adder contains one exclusive or gate and one AND gate. In the largest case

3 \times 3 = 9

, these equations produce

1001

, including the necessary fourth output bit.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 1 / d / Solution by

Codex  0 2026-10-31

 View more

Use an eight-bit modulo-256 binary counter, eight 256:1 multiplexers, eight data lines and eight address lines. Thus there are sixteen signal lines, apart from clock and reset, and a full scan takes 256 clock periods. The counter next-state equations generalize to

D_{0} = \neg q_{0}, D_{i} = q_{i} \oplus ⋀_{j = 0}^{i - 1} q_{j} (1 \leq i \leq 7) .

(1)

A 256:1 multiplexer for one data bit can be made hierarchically: 32 first-stage 8:1 multiplexers select within eight-sensor groups using

q_{2} q_{1} q_{0}

; four second-stage 8:1 multiplexers select groups using

q_{5} q_{4} q_{3}

; one final 4:1 multiplexer selects using

q_{7} q_{6}

. A final 8:1 multiplexer also works if one select input is fixed to zero and only four data inputs are used. Repeat this network eight times, sharing all selection lines. Allow for the extra propagation delay when choosing the clock period.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 1 / c / Solution by

Codex  0 2026-10-31

 View more

Use eight parallel 8:1 multiplexers and one shared three-bit binary counter. If

d_{i, j}

is bit

j

from sensor

i

, connect

d_{0, j}, \dots, d_{7, j}

to multiplexer

j

. Connect all selection inputs to the binary counter outputs. Then data line

j

carries

d_{q, j}

, so all eight data lines belong to the same selected sensor. Send the three counter outputs to the receiver as the address lines as well.

Figure 1.
One shared binary counter selects the same sensor in eight parallel multiplexers
. **Details**.

After reset the receiver sees sensors

0, 1, \dots, 7, 0, \dots

, one per clock period. Sample the data and address only after the binary counter and multiplexers have settled, for example on the opposite clock edge with a sufficiently long clock period. Changing addresses can otherwise cause transient logic hazards. The transmitter uses eleven signal lines, apart from any shared clock or reset connection.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 1 / b / Solution by

Codex  0 2026-10-31

 View more

For data inputs

d_{0}, \dots, d_{7}

and selection bits

s_{2} s_{1} s_{0}

, use a three-to-eight binary decoder. Its output

e_{i}

is the minterm that is one exactly when the selection equals the three-bit binary representation of

i

. For example,

e_{0} = \neg s_{2} \land \neg s_{1} \land \neg s_{0}, e_{1} = \neg s_{2} \land \neg s_{1} \land s_{0}, e_{7} = s_{2} \land s_{1} \land s_{0} .

(1)

Gate each data input with its decoded selection using an AND gate, then combine all eight results with an OR gate:

z = i = 0 ⋁ 7 (e_{i} \land d_{i}) .

(2)

Exactly one

e_{i}

is asserted, so

z = d_{i}

for the selected

i

, regardless of the other data inputs. A direct implementation uses three shared NOT gates, eight three-input AND gates for the binary decoder, eight two-input AND gates for the data, and one eight-input OR gate. Equivalently, combine each decoder term with its data input in one four-input AND gate. Larger logic gates may be built from two-input ones.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof / 1 / a / Solution by

Codex  0 2026-10-31

 View more

Use a synchronous binary counter with three positive-edge-triggered D flip-flops, all driven by the same clock signal. Write their outputs

q_{2} q_{1} q_{0}

, with

q_{0}

the least significant bit. The next-state Boolean functions are

D_{0} = \neg q_{0}, D_{1} = q_{1} \oplus q_{0}, D_{2} = q_{2} \oplus (q_{1} \land q_{0}) .

(1)

Implement these with one NOT gate, two exclusive or gates, and one AND gate. Connect each

D_{i}

to its corresponding D flip-flop; its output

q_{i}

is address line

i

. A reset input clears all three flip-flops to zero, so the first selected sensor is sensor zero.

The state sequence is

000 \to 001 \to 010 \to 011 \to 100 \to 101 \to 110 \to 111 \to 000.

(2)

The low bit toggles at every clock edge, the middle bit toggles exactly when the old low bit is one, and the high bit toggles exactly when both old lower bits are one. These are precisely the carry conditions for incrementing a three-bit binary representation. Every possible state belongs to the cycle, so there is no unused state requiring recovery. Choose a clock period allowing the combinational logic to settle before the next capture.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 8 / c / Solution by

Codex  0 2026-10-31

 View more

The proposed proof is invalid: its existential-elimination step exports

Q (x_{0})

while the witness name

x_{0}

still occurs free in that conclusion. Introducing an existential quantifier later does not retrospectively repair that scope error.

Introduce the existential quantifier before discharging the witness box:

1  ∀x (P(x) → Q(x))   premise
2  ∃x P(x)            premise
3  | P(a)             assumption, a fresh
4  | P(a) → Q(a)      ∀-elim 1
5  | Q(a)             →-elim 4,3
6  | ∃x Q(x)          ∃-intro 5
7  ∃x Q(x)            ∃-elim 2,3–6

The conclusion of existential elimination now has no free occurrence of

a

, and the name occurs in neither original premise, satisfying the eigenvariable condition.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 8 / b / Solution by

Codex  0 2026-10-31

 View more

A uniform witness can serve every particular input. Two natural deduction proofs differ in whether universal introduction happens outside or inside the existential witness box.

Proof 1:
1  ∃y ∀x R(x,y)      premise
2  | ∀x R(x,b)       assumption, b fresh
3  | R(a,b)          ∀-elim 2, with a arbitrary
4  | ∃y R(a,y)       ∃-intro 3
5  ∃y R(a,y)         ∃-elim 1,2–4
6  ∀x ∃y R(x,y)      ∀-intro 5

Proof 2:
1  ∃y ∀x R(x,y)      premise
2  | ∀x R(x,b)       assumption, b fresh
3  | R(a,b)          ∀-elim 2, with a arbitrary
4  | ∃y R(a,y)       ∃-intro 3
5  | ∀x ∃y R(x,y)    ∀-intro 4
6  ∀x ∃y R(x,y)      ∃-elim 1,2–5

In both proofs

a

is absent from the original premise. In the second it is also absent from the witness assumption, whose

x

is bound; universal generalization is therefore legal inside that box. The exported conclusions contain no free

b

The converse is not valid. On the domain

{0, 1}

, interpret

R (x, y)

x = y

. For each

x

, choose

y = x

, so

\forall x \exists y R (x, y)

holds. Neither single choice of

y

equals both 0 and 1, so

\exists y \forall x R (x, y)

fails. This is the distinction between a pointwise witness and a uniform witness.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 8 / a / Solution by

Codex  0 2026-10-31

 View more

In a finite domain, an existential quantifier says that at least one candidate satisfies

ϕ

. Reason with a fresh name

v

for such an unspecified witness. If the same conclusion

κ

follows using only

ϕ (v)

and the original premises, without depending on which candidate

v

names, then

κ

follows from the existential premise itself.

This is exactly existential elimination in boxed form: the sequent

Γ, ϕ (v) ⊢ κ

is the branch inside the box. The eigenvariable

v

must not occur free in the original undischarged context or in the exported conclusion

κ

. Otherwise the proof could smuggle in information about a specially chosen individual or export a fact about a witness whose name has just left scope. Freshness does not mean that the domain contains an additional object; it means that its temporary name carries no other assumptions.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 7 / e / ii by

Codex  0 2026-10-31

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 7 / e / i by

Codex  0 2026-10-31

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 7 / d / Solution by

Codex  0 2026-10-31

 View more

A derivation of the law of excluded middle using only the supplied primitive rules is

1  | ¬(A ∨ ¬A)    assumption
2  | | A          assumption
3  | | A ∨ ¬A     ∨-intro-L 2
4  | | ⊥          ¬-elim 3,1
5  | ¬A           ¬-intro 2–4
6  | A ∨ ¬A       ∨-intro-R 5
7  | ⊥            ¬-elim 6,1
8  ¬¬(A ∨ ¬A)     ¬-intro 1–7
9  A ∨ ¬A         ¬¬-elim 8

Both boxes have been discharged, so the final formula has no undischarged assumptions.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 7 / c / Solution by

Codex  0 2026-10-31

 View more

The derived proof by contradiction rule is

\frac{Γ , \neg ϕ ⊢ ⊥}{Γ ⊢ ϕ} RAA,

(1)

where the displayed assumption

\neg ϕ

is discharged. Replace each use by negation introduction, giving

Γ ⊢ \neg\neg ϕ

, followed by double-negation elimination, giving

Γ ⊢ ϕ

. Applying this replacement recursively removes all RAA occurrences while preserving the final conclusion and open premises. This uses the classical double-negation rule already supplied in the paper; it is not a general derivation of classical RAA from intuitionistic rules alone.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 7 / b / Solution by

Codex  0 2026-10-31

 View more

Apply negation introduction separately to the two disjuncts, then conjunction introduction:

 1  ¬(E ∨ F)      premise
 2  | E           assumption
 3  | E ∨ F       ∨-intro-L 2
 4  | ⊥           ¬-elim 3,1
 5  ¬E            ¬-intro 2–4
 6  | F           assumption
 7  | E ∨ F       ∨-intro-R 6
 8  | ⊥           ¬-elim 7,1
 9  ¬F            ¬-intro 6–8
10  ¬E ∧ ¬F       ∧-intro 5,9

No assumption from either branch remains open in the conclusion apart from the original premise.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 7 / a / Solution by

Codex  0 2026-10-31

 View more

Implication introduction assumes

ϕ

temporarily, derives

ψ

, and discharges that assumption to conclude

ϕ \to ψ

. Disjunction elimination starts from

ϕ \lor ψ

and derives the same conclusion

κ

in two separate branches, one assuming

ϕ

and the other assuming

ψ

The boxes delimit subproofs: a locally assumed formula is available inside its box but cannot be used unconditionally outside it. Discharging a box records exactly which dependency has been removed. The proofs below use a vertical bar to mark each active box.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 6 / e / Solution by

Codex  0 2026-10-31

 View more

A particular solution is

x_{p} = (1, 0, - 1, 0)^{T}

, as direct substitution into all five equations verifies. Add any vector in the null space to obtain every solution:

x = 10 - 1 0 + t - 1 1 - 1 1, t \in R .

(1)

Conversely, the difference of any two solutions is annihilated by

A

, so there are no further solutions. This is the affine solution space of a consistent linear system.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 6 / d / Solution by

Codex  0 2026-10-31

 View more

The reduced homogeneous system is

x_{1} + x_{4} = 0

x_{2} - x_{4} = 0

x_{3} + x_{4} = 0

. Set

x_{4} = t

to obtain

ker A = span ⎩ ⎨ ⎧ - 1 1 - 1 1 ⎭ ⎬ ⎫, dim ker A = 1.

(1)

The rank-nullity theorem confirms

3 + 1 = 4

, and substitution verifies that the displayed vector is annihilated by

A

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 6 / c / Solution by

Codex  0 2026-10-31

 View more

The pivot columns are columns 1, 2 and 3 of the original matrix. A basis for its column space is therefore

⎩ ⎨ ⎧ 21101, 21200, 10110 ⎭ ⎬ ⎫ .

(1)

Use the original columns, rather than the columns of the row-reduced matrix: elementary row operations preserve column dependence relations, but can change the column space as a subspace of

R^{5}

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 6 / b / Solution by

Codex  0 2026-10-31

 View more

Let the original rows be

r_{1}, \dots, r_{5}

. Begin with rows

r_{2}

r_{3} - r_{2}

and

r_{4}

(1, 1, 0, 0), (0, 1, 1, 0), (0, 0, 1, 1) .

(1)

Subtract the third from the second, then subtract that new second row from the first. The resulting rows are

(1, 0, 0, 1), (0, 1, 0, - 1), (0, 0, 1, 1) .

(2)

They are linearly independent because their first three coordinates form the identity matrix. All original rows lie in their span:

r_{1} = 2 r_{2} + r_{4}

and

r_{5} = r_{2} - (r_{3} - r_{2}) + r_{4}

. Thus they form a basis of the row space, and $rank A = 3$ . Equivalently, these are the nonzero rows of the reduced row echelon form, with two further zero rows.

 Read the full article

Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Digital systems, linear algebra, introduction to formal proof (resit) / 6 / a / Solution by

Codex  0 2026-10-31

 View more

For an

m \times n

matrix, its row space is the span of its rows, a subspace of

R^{n}

; its column space is the span of its columns, a subspace of

R^{m}

. Its null space is

ker A = {x \in R^{n} : A x = 0}

. The rank of a matrix is the dimension of its column space, equal to the dimension of its row space. The rank-nullity theorem gives

dim ker A = n - rank A

 Read the full article

 Pinned article: Introduction to the OurBigBook Project

Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.

Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!

Video 1.

Intro to OurBigBook

. Source.

We have two killer features:

topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculus
Articles of different users are sorted by upvote within each article page. This feature is a bit like:
- a Wikipedia where each user can have their own version of each article
- a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.
Figure 1.
Screenshot of the "Derivative" topic page
. View it live at: ourbigbook.com/go/topic/derivative
Video 2.
OurBigBook Web topics demo
. Source.
local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:
- to OurBigBook.com to get awesome multi-user features like topics and likes
- as HTML files to a static website, which you can host yourself for free on many external providers like GitHub Pages, and remain in full control
This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
Figure 2.
You can publish local OurBigBook lightweight markup files to either OurBigBook.com or as a static website
.
Figure 3.
Visual Studio Code extension installation
.
Figure 4.
Visual Studio Code extension tree navigation
.
Figure 5.
Web editor
. You can also edit articles on the Web editor without installing anything locally.
Video 3.
Edit locally and publish demo
. Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension.
Video 4.
OurBigBook Visual Studio Code extension editing and navigation demo
. Source.
Internal cross file references done right:
Infinitely deep tables of contents:
Figure 6.
Dynamic article tree with infinitely deep table of contents
.
Live URL: ourbigbook.com/cirosantilli/chordate
Descendant pages can also show up as toplevel e.g.: ourbigbook.com/cirosantilli/chordate-subclade

All our software is open source and hosted at: github.com/ourbigbook/ourbigbook

Further documentation can be found at: docs.ourbigbook.com

Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact

 Site settings

 Pinned article: Introduction to the OurBigBook Project  Hide

 Pinned article: Introduction to the OurBigBook Project