[ slides ] add slides

Author: bobatkey

.gitignore

@@ -3,3 +3,11 @@
 /_build/
 /_site/
 /target
+/slides/*.nav
+/slides/*.aux
+/slides/*.log
+/slides/*.out
+/slides/*.pdf
+/slides/*.snm
+/slides/*.toc
+/slides/*.upa

flake.nix

@@ -12,6 +12,23 @@
     flake-utils.lib.eachDefaultSystem (system:
       let
         pkgs = nixpkgs.legacyPackages.${system};
+
+        tex = pkgs.texlive.combine {
+          inherit (pkgs.texlive)
+            # https://tug.org/texlive/devsrc/Master/doc.html
+            scheme-minimal latex-bin xetex latexmk beamer
+            infwarerr kvoptions latex-tools-dev
+
+            libertine
+
+            mathpartir stmaryrd frankenstein multirow
+            colortbl cmll euler fontspec tools extsizes
+            minibox varwidth fragments psnfss csquotes
+            ulem xltxtra realscripts booktabs todonotes
+            pdfcomment datetime2 tracklang zref marginnote
+            soulpos appendixnumberbeamer; # soulutf8;
+        };
+
         on = opam-nix.lib.${system};
         localPackagesQuery = builtins.mapAttrs (_: pkgs.lib.last)
           (on.listRepo (on.makeOpamRepo ./.));
@@ -50,18 +67,37 @@
         packages =
           pkgs.lib.getAttrs (builtins.attrNames localPackagesQuery) scope';
       in {
-        legacyPackages = scope';
+        # legacyPackages = scope';
+
+        #inherit packages;
+
+        packages = packages // { slides = pkgs.stdenvNoCC.mkDerivation rec {
+          name = "slides";
+          src = self;
+          buildInputs = [ pkgs.coreutils pkgs.bash tex pkgs.libertine pkgs.gnumake ];
+          phases = ["unpackPhase" "buildPhase" "installPhase"];
+          buildPhase = ''
+export PATH="${pkgs.lib.makeBinPath buildInputs}";
+mkdir -p .cache/texmf-var;
+export TEXMFHOME=.cache;
+export TEXMFVAR=.cache/texmf-var;
+make -C slides -j 8 all
+'';
+          installPhase = ''
+mkdir -p $out;
+cp slides/week*.pdf $out/;
+'';
+        }; };
 
-        inherit packages;
 
-        ## If you want to have a "default" package which will be built with just `nix build`, do this instead of `inherit packages;`:
-        # packages = packages // { default = packages.slakemoth; };
+                   # // { default = packages.slakemoth; };
 
         devShells.default = pkgs.mkShell {
           inputsFrom = builtins.attrValues packages;
           buildInputs = devPackages ++ [
             pkgs.rsync
             # You can add packages from nixpkgs here
+            tex
           ];
         };
       });

slides/800px-Plato_Silanion_Musei_Capitolini_MC1377.jpg

@@ -0,0 +1,9 @@
+.PHONY: clean all
+
+all: week1.pdf week2.pdf week3.pdf week4.pdf week5.pdf week6.pdf week7.pdf week8.pdf week9.pdf week10.pdf
+
+week%.pdf: week%.tex macros.tex strathclyde.sty
+	latexmk -xelatex $<
+
+clean:
+	rm -f *.pdf *.aux *.log *.xdv *.fls *.nav *.fdb_latexmk *.out *.toc *.snm *.upa

slides/Luitzen_Egbertus_Jan_Brouwer.jpeg

@@ -0,0 +1,237 @@
+% -*- TeX-engine: xetex -*-
+
+\documentclass[xetex,aspectratio=169,14pt,hyperref={pdfpagelabels=true,pdflang={en-GB}}]{beamer}
+
+\input{macros}
+
+\title[CS208 - Introduction]{CS208 (Semester 1) : Introduction}
+
+\begin{document}
+
+\maketitle
+
+\section{Introduction}
+
+\begin{frame}{CS208 : Logic and Algorithms}
+
+  In this semester we will study \emph{Symbolic Logic}.
+
+  \bigskip
+
+  \begin{enumerate}
+  \item What is a good language for formal statements?
+  \item What are valid rules of inference?
+  \item How can we relate situations and statements about them?
+  \end{enumerate}
+\end{frame}
+
+\begin{frame}
+  {Very rough History of Logic}
+
+  (with a Western bias)
+
+  \bigskip
+
+  \begin{tabular}{ll}
+    \textcolor{black!60}{$\sim$350BCE}& Aristotle's \emph{Organon} (``\emph{logos}'' = ``the word'') \\
+    \textcolor{black!60}{300BCE-1847CE}& Lots of interesting but scattered stuff... \\
+    \textcolor{black!60}{1847} & George Boole's \emph{Mathematical Analysis of Logic} \\
+%                & \quad later \emph{An Investigation of the Laws of Thought...} \\
+    \textcolor{black!60}{1879} & Gottlob Frege's \emph{Begriffsschrift} \\
+ %               & \quad invention of \emph{Quantifiers} \\
+    \textcolor{black!60}{1880s to 1930s} & Logic\textbf{s} as an object of study in their own right\\
+  %              & \quad Kurt G{\"o}del, Alfred Tarski, Alan Turing, ...\\
+    \textcolor{black!60}{1940s to date} & Explosion, especially driven by CS.
+  \end{tabular}
+\end{frame}
+
+\begin{frame}
+  {Why study Logic?}
+
+  Logic is \emph{extremely useful} in Computer Science.
+
+  \bigskip
+
+  For example...
+  \begin{enumerate}
+  \item Digital circuits
+  \item Specifying systems' behaviour
+  \item Proving that systems satisfy their specifications
+  \item Automated Reasoning, rule-based AI
+  \item Designing Programming Languages
+  \item Database Query Languages
+  \end{enumerate}
+\end{frame}
+
+\begin{frame}
+  {In this course}
+
+  We will cover two major sorts of Logic:
+
+  \begin{enumerate}
+  \item Propositional Logic
+  \item Predicate Logic
+  \end{enumerate}
+\end{frame}
+
+\begin{frame}
+  {Propositional Logic}
+
+  Propositional Logic talks about atomic statements:
+  \begin{mathpar}
+    \textit{``it is raining''}
+
+    \textit{``I am in Glasgow''}
+  \end{mathpar}
+  and compound statements made from those:
+  \begin{mathpar}
+    \textit{``it is raining''} \land \textit{``I am in Glasgow''}
+
+    \textit{``it is raining''} \to \textit{``I am in Glasgow''}
+  \end{mathpar}
+
+\end{frame}
+
+\begin{frame}
+  {Predicate Logic}
+
+  Predicate Logic adds \emph{quantifiers} and \emph{predicates}:
+  \begin{mathpar}
+    \forall \mathit{day}.~\textrm{InGlasgow}(\mathit{day}) \to (\textrm{Raining}(\mathit{day}) \lor \textrm{Drizzle}(\mathit{day}))
+
+    \forall x. \forall y.~x + y = y + x
+  \end{mathpar}
+\end{frame}
+
+\begin{frame}
+  {Semantics}
+
+  The \emph{Semantics} of a logic tell you what formulas \emph{mean}.
+
+  \bigskip
+
+  Roughly, we will take the view that a formula's meaning is the
+  collection of situations that make it true.
+  \begin{mathpar}
+    \sem{G \lor R} = \left\{
+      \begin{array}{@{}l}
+        \{G \mapsto \true, R \mapsto \false\}, \\
+        \{G \mapsto \false, R \mapsto \true\}, \\
+        \{G \mapsto \true, R \mapsto \true\}
+      \end{array}
+    \right\}
+
+    \sem{G \land R} = \left\{ [G \mapsto \true,R \mapsto \true] \right\}
+  \end{mathpar}
+\end{frame}
+
+\begin{frame}
+  {Logical Modelling}
+
+  A fundamental use for logic is to create models of situations.
+
+  \bigskip
+
+  \begin{enumerate}
+  \item Encode potential facts as atomic statements:
+    \begin{itemize}
+    \item $\mathsf{cell}((3,3), 4)$ -- cell $(3,3)$ of a sudoku board contains $4$.
+    \item $\mathsf{assigned}(A,M)$ -- task $A$ is assigned to machine $M$.
+    \item $\mathsf{installed}(progA, 1)$ -- version 1 of program A is installed
+    \end{itemize}
+  \item Encode constraints as logical statements:
+    \begin{itemize}
+    \item $\mathsf{installed}(progA,1) \to (\mathsf{installed}(libB,3) \land \mathsf{installed}(libC,2))$ \\
+      -- program A v1 requires libB v3 and libC v2.
+    \end{itemize}
+  \item Finding a true/false value for each atom that makes all the
+    constraints true allows us to solve the problem.
+  \end{enumerate}
+\end{frame}
+
+\begin{frame}
+  {Deductive Systems}
+
+  \emph{Deductive Systems} are collections of rules that allow you to
+  derive valid statements from valid statements.
+
+  \bigskip
+
+  A rule:
+  \begin{displaymath}
+    \inferrule*
+    {X\textit{ is feathery} \\ X\textit{ lays eggs}}
+    {X\textit{ is a bird}}
+  \end{displaymath}
+
+  Above the line are \emph{premises}, below is the \emph{conclusion}.
+
+  \bigskip
+
+  We will study rules for Propositional and Predicate Logic.
+\end{frame}
+
+\begin{frame}
+  {Course plan}
+
+  \begin{tabular}{ll}
+    Week 1 & Recap Propositional Logic \\
+    Week 2 & Logical modelling and SAT solvers \\
+    Week 3 & More examples of Logical Modelling \\
+    Week 4 & More examples of Logical Modelling \\
+    Week 5 & Deductive proof for Propositional Logic \\
+    Week 6 & Predicate Logic \\
+    Week 7 & Deductive proof for Predicate Logic \\
+    Week 8 & Semantics of Predicate Logic \\
+    Week 9 & Equality and Arithmetic in Predicate Logic \\
+    Week 10 & Metatheory \\
+  \end{tabular}
+\end{frame}
+
+\begin{frame}
+  {Course Delivery}
+
+  For Semester 1:
+  \begin{itemize}
+  \item \textbf{Lectures}: two/week \\
+    Mondays 12:00-13:00, GH514 \\
+    Fridays 12:00-13:00, RC512
+  \item \textbf{Video minilectures}: roughly four/week, roughly ten minutes each.
+  \item \textbf{Notes and Tutorial Exercises}: linked from MyPlace.
+  \item \textbf{Tutorials}: Mondays and Fridays, assignment to follow.
+  \item \textbf{Mattermost chat}: use the Mattermost channel for this
+    course to discuss the course and ask questions.
+  \item \textbf{Individual questions}: contact the course lecturer.
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  {Assessment}
+
+  The whole course (Semesters 1\&2) is 30\% coursework, 70\% exam.
+
+  \bigskip
+
+  This semester there are two courseworks:
+  \begin{center}
+    \begin{tabular}{llll}
+      Name & Release & Submission & Weighting\\
+      \hline
+      1 : Logical Modelling &Wed 4th Oct &Wed 18th Oct &7.5 \% \\
+      2 : Deductive Proof   &Wed 2nd Nov &Wed 30th Nov &7.5 \%\\
+    \end{tabular}
+  \end{center}
+
+  \bigskip
+
+  Single exam for Logic and Algorithms in April/May.
+\end{frame}
+
+\begin{frame}
+  \begin{center}
+    {\Huge Hope you enjoy the course!} \\
+    Check MyPlace for course arrangements and updates.
+  \end{center}
+\end{frame}
+
+\end{document}

slides/Makefile

@@ -0,0 +1,98 @@
+\usepackage[sci,noslidestrathidentity]{strathclyde}
+\strathsetidentity{Department of}{Computer \& Information Sciences}
+
+\usepackage{lmodern}
+\usepackage{subscript}
+\usepackage{url}
+\usepackage{pifont}
+\usepackage{csquotes}
+\usepackage{mathpartir}
+\usepackage{stmaryrd}
+\usepackage{multirow}
+\usepackage{euler}
+\usepackage[normalem]{ulem}
+
+% 2013-09-08 SU adding xetex specifics
+% http://www.woggie.net/2008/07/16/beamer-pdftex-and-xetex/
+\usepackage{xltxtra}
+
+% 2013-09-08 SU http://robjhyndman.com/hyndsight/xelatex/
+\defaultfontfeatures{Ligatures=TeX}
+
+% 2015-12-09 SU table beautified
+\renewcommand{\arraystretch}{1.2}
+\usepackage{booktabs}
+
+%MGK compatibility
+\newcommand{\hh}[1]
+  {\medskip\textbf{\large #1}}
+\newcommand{\pdu}[3]
+  {#1\rightarrow #2 : &\ & \makebox[70mm][l]{$#3$}}
+
+
+
+\setlength{\marginparwidth}{2cm}
+\usepackage{todonotes}%[disable]
+\let\OldTodo\todo
+\renewcommand{\todo}{\OldTodo[inline]}%
+\newcommand{\todolater}[1]{}% Things to do for next year
+
+
+\DeclareTextCommandDefault{\nobreakspace}{\leavevmode\nobreak\ }
+\usepackage{rotating}
+
+\usepackage{pdfcomment}% To add alt text for images using \pdftooltip{}
+
+\usepackage{appendixnumberbeamer}
+
+\newcommand{\messageframe}[1]{\begin{frame}\begin{center}\Huge #1\end{center}\end{frame}}
+\newcommand{\sechead}[1]{{\bf #1} \\}
+\newcommand{\examplehead}[1]{{\bf Example:} {\it\textcolor{red!90}{#1}} \\}
+\newcommand{\eqnote}[1]{\hspace{3cm}\textit{#1}}
+\newcommand{\sidenote}[1]{\qquad {\footnotesize \textcolor{black!60}{(#1)}}}
+\newcommand{\sem}[1]{\llbracket #1 \rrbracket}
+\newcommand{\true}{\mathsf{T}}
+\newcommand{\false}{\mathsf{F}}
+
+\def\strikeafter<#1>#2{\temporal<#1>{#2}{\sout{#2}}{\sout{#2}}}
+
+
+%\newcommand{\rhighlight}{\textcolor{titlered}}
+\newcommand{\rhighlight}{\textbf}
+\newcommand{\highlight}{\textbf}
+
+% \setmainfont{Linux Biolinum O}
+\setmainfont{LinBiolinum}[
+Path=,
+UprightFont = *_R.otf ,
+BoldFont = *_RB.otf ,
+ItalicFont = *_RI.otf
+]
+
+\setbeamertemplate{navigation symbols}{}
+%\usecolortheme[rgb={0.8,0,0}]{structure}
+\usefonttheme{serif}
+\usefonttheme{structurebold}
+\setbeamercolor{description item}{fg=black}
+
+
+\author[Atkey]{Dr.~Robert Atkey}
+\institute[Strathclyde]{Computer \& Information Sciences}
+\date[]{}
+
+\newcommand{\weeksection}[1]{%
+  \section{\thetitle{}, Part~\thesection : #1}
+  \begin{frame}
+    \begin{center}
+      \textcolor{black!60}{\thetitle{}, Part \thesection}\\
+      {\Huge #1}
+    \end{center}
+  \end{frame}}
+
+\newcommand{\weektitle}[2]{\def\thetitle{#2}
+\title[CS208 - Week #1]{CS208 (Semester 1) Week #1 : #2}}
+
+\newcommand{\assigned}{:}
+
+\newcommand{\forcedto}{\assigned_f}
+\newcommand{\decideto}{\assigned_d}