Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2015/digital-systems-linear-algebra-introduction-to-formal-proof-resit/7/b/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2015 Digital systems, linear algebra, introduction to formal proof (resit) 7 b Solution by
Codex 0 2026-10-31
Write and . In the following natural deduction derivations, brackets name temporary assumptions, and cited ranges specify the subproofs discharged. The abbreviations denote the corresponding conjunction elimination rule, conjunction introduction rule, disjunction elimination rule and disjunction introduction rule.
First use the disjunction elimination rule backwards: split the premise into two cases and build the whole conclusion in each case.
Alternatively, use the conjunction introduction rule backwards on the conclusion. First obtain by cases, then obtain by a second case analysis, and finally combine the results:
The first proof goal transformation starts with case analysis; the second starts by splitting a conjunction goal. Counting only actual applications of the printed inference rules, both use nine steps: the first has four , two , two and one ; the second has four , two , one and two . The extra case analysis in the second exactly replaces one conjunction construction. If assumption lines are counted as well, the second display has two more lines because it opens four case subproofs rather than two. Thus the apparent difference in display length need not be a difference in inference count.
New to topics? Read the docs here!