forked from OpenLogicProject/forallx-cam
-
Notifications
You must be signed in to change notification settings - Fork 34
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
adjust wording slighlty; move accessibility appendix to its own file
- Loading branch information
Showing
5 changed files
with
130 additions
and
124 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,120 @@ | ||
%!TEX root = forallxyyc.tex | ||
|
||
\chapter{Notes on accessibility} | ||
|
||
Special attention has been paid to make this HTML version as | ||
accessible as possible, especially to readers using Assistive | ||
Technology (AT), such as screen readers. It has, however, not | ||
been extensively tested. If you are using it with a screen reader or | ||
Braille terminal, or are helping a student who relies on such tools | ||
(e.g., as instructor or accessibility advisor), and you have feedback | ||
please \href{mailto:[email protected]}{get in touch}! | ||
|
||
\paragraph{Navigation and styles} We have adopted the HTML style | ||
provided by \href{https://vlmantova.github.io/bookml/}{BookML}, | ||
developed for the Leeds mathematics department by | ||
\href{https://eps.leeds.ac.uk/maths/staff/4058/dr-vincenzo-l-mantova}{Vincenzo | ||
Mantova}. It provides a collapsible navigation menu, buttons at the | ||
top of each page to select the font size, switch between serif and | ||
sans-serif font, and black-on-white, dark-on-sepia, or light-on-dark | ||
display options. | ||
|
||
\paragraph{Symbols and formulas} All logical symbols and formulas in | ||
this book are converted to MathML and displayed using | ||
\href{https://www.mathjax.org/}{MathJax}. MathJax provides additional | ||
\href{https://docs.mathjax.org/en/latest/basic/accessibility.html}{accessibility | ||
features} for formulas, which are found in the MathJax context | ||
menu---activate/right click on any formula to activate it. If your | ||
screen reader does not read out formulas such as $\forall x(A(x) \land | ||
B(x))$ you may need to activate Speech Output in the Speech submenu of | ||
the MathJax accessibility menu. | ||
|
||
For reference, here is a table of all the symbols used in the text, | ||
how they are (probably?) pronounced, and what they are called in the | ||
text. In the rightmost column we provide a suggested way to enter them | ||
using ASCII characters, if inserting special symbols (in a homework | ||
assignment or email to your instructor, say) is not an option. | ||
|
||
\begin{tabular}{lllll} | ||
\lxBeginTableHead{}Symbol\lxTableColumnHead{} & Pronounciation\lxTableColumnHead{} & Meaning\lxTableColumnHead{} & ASCII equivalent\lxTableColumnHead{}\\ | ||
\hline\lxEndTableHead | ||
$\enot$ & not sign & logical not & \verb+~+ or \verb+-+\\ | ||
$\eor$ & or & logical or & \verb+\/+\\ | ||
$\eand$ & and & logical and & \verb+/\+ or \verb+&+\\ | ||
$\eif$ & right arrow & conditional & \verb+->+ or \verb+>+\\ | ||
$\eiff$ & left right arrow & biconditional & \verb+<->+ or \verb+<>+\\ | ||
$\ered$ & up tack & contradiction & \verb+_|_+ or \verb+!?+\\ | ||
$\forall$ & for all & universal quantifier & \verb|A| or \verb|@|\\ | ||
$\exists$ & there exists & existential quantifier & \verb|E| or \verb|3|\\ | ||
$\therefore$ & therefore & therefore & \verb|:.|\\ | ||
$\proves$ & right tack & proves & \verb+|-+\\ | ||
$\nproves$ & does not prove & does not prove & \verb+|/-+\\ | ||
$\entails$ & true & entails & \verb+|=+\\ | ||
$\nentails$ & not true & does not entail & \verb+|/=+\\ | ||
$\ebox$ & white square & necessary & \verb+[]+\\ | ||
$\ediamond$ & white diamond & possible & \verb+<>+ | ||
\end{tabular} | ||
|
||
Subscripts should be pronounced by screen readers, although | ||
if the subscript is a number, they may not be. They can be | ||
represented by an underline, e.g., $A_2$ as \verb|A_2|. | ||
|
||
The expressions `\blank{}' and `\ifeff' are used throughout the textbook. | ||
`Iff' is short for `if and only if'. The HTML versions of both are | ||
provided with ARIA labels to help screen readers pronounce them | ||
properly (i.e., as `blank' and `if-eff'). | ||
|
||
\paragraph{Proofs} The natural deduction proofs in | ||
\cref{ch.NDTFL,ch.NDFOL,ch.ML} use vertical lines to indicate where | ||
subproofs start and end. Such vertical lines extend from the | ||
assumption line of the subproof to its last line and are displayed | ||
between the line numbers and the formulas in any given line. This | ||
makes proofs a special challenge for users with low vision or complete | ||
loss of vision. | ||
|
||
To make these proofs accessible in this HTML version, proofs are coded | ||
as tables. Each table line has four columns: the line number, a | ||
subproof level indicator, a formula, and a justification. The subproof | ||
level indicator is a number recording how many nested subproofs the | ||
current line is contained in. It is 0 if the line is not contained in | ||
a subproof, 1 if it is in a subproof, 2 if it is in a subproof nested | ||
within another subproof, and so on. When reading out a subproof level | ||
indicator, screen readers should also announce if a subproof has just | ||
been closed on the previous line, and when a new subproof starts. The | ||
table header rows and subproof level indicators are hidden so that | ||
proofs visually appear as in the printed text. | ||
|
||
Here is an example of such a proof: | ||
\begin{fitchproof} | ||
\hypo{wxyz}{(W \eor X) \eor (Y \eor Z)}\PR | ||
\hypo{xy}{X \eif Y}\PR | ||
\hypo{nz}{\enot Z}\PR | ||
\open | ||
\hypo{wx}{W \eor X}\AS | ||
\open | ||
\hypo{w}{W}\AS | ||
\have{wy1}{W \eor Y}\oi{w} | ||
\close | ||
\open | ||
\hypo{x}{X}\AS | ||
\have{y1}{Y}\ce{xy, x} | ||
\have{wy2}{W \eor Y}\oi{y1} | ||
\close | ||
\have{wy3}{W \eor Y}\oe{wx, w-wy1, x-wy2} | ||
\close | ||
\open | ||
\hypo{yz}{Y \eor Z}\AS | ||
\have{y}{Y}\ds{yz, nz} | ||
\have{wy}{W \eor Y}\oi{y} | ||
\close | ||
\have{wy4}{W \eor Y}\oe{wxyz, wx-wy3, yz-wy} | ||
\end{fitchproof} | ||
It has 14 lines, with 3 premises, 2 levels of subproof nesting, and | ||
two pairs of adjacent subproofs. For instance, the subproof beginning | ||
on line 5 ends at line 6, and line 7 starts another subproof. So the | ||
subproof levels of lines 6 and 7 is the same, but lines 6 and 7 are in | ||
different subproofs. If you cannot see the subproof lines, you have to | ||
pay special attention to how the subproof level numbers change | ||
\emph{and} when a formula is an assumption. A screen reader should | ||
announce line 7 as ``7, close subproof, 2, open subproof, $X$, | ||
AS.'' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -45,122 +45,4 @@ | |
|
||
\input{forallx-yyc-content} | ||
|
||
\chapter{Notes on accessibility} | ||
|
||
Special attention has been paid to make this HTML version as | ||
accessible as possible, especially to readers using Assistive | ||
Technology (AT), such as screen readers. It has, however, not | ||
been extensively tested. If you are using it with a screen reader or | ||
Braille terminal, or are helping a student who relies on such tools | ||
(e.g., as instructor or accessibility advisor), and you have feedback | ||
please \href{mailto:[email protected]}{get in touch}! | ||
|
||
\paragraph{Navigation and styles} We have adopted the HTML style | ||
provided by \href{https://vlmantova.github.io/bookml/}{BookML}, | ||
developed for the Leeds mathematics department by | ||
\href{https://eps.leeds.ac.uk/maths/staff/4058/dr-vincenzo-l-mantova}{Vincenzo | ||
Mantova}. It provides a collapsible navigation menu, buttons at the | ||
top of each page to select the font size, switch between serif and | ||
sans-serif font, and black-on-white, dark-on-sepia, or light-on-dark | ||
display options. | ||
|
||
\paragraph{Symbols and formulas} All logical symbols and formulas in | ||
this book are converted to MathML and displayed using | ||
\href{https://www.mathjax.org/}{MathJax}. MathJax provides additional | ||
\href{https://docs.mathjax.org/en/latest/basic/accessibility.html}{accessibility | ||
features} for formulas, which are found in the MathJax context | ||
menu---activate/right click on any formula to activate it. If your | ||
screen reader does not read out formulas such as $\forall x(A(x) \land | ||
B(x))$ you may need to activate Speech Output in the Speech submenu of | ||
the MathJax accessibility menu. | ||
|
||
For reference, here is a table of all the symbols used in the text, | ||
how they are (probably?) pronounced, and what they are called in the | ||
text. In the rightmost column we provide a suggested way to enter them | ||
using ASCII characters, if inserting special symbols (in a homework | ||
assignment or email to your instructor, say) is not an option. | ||
|
||
\begin{tabular}{lllll} | ||
\lxBeginTableHead{}Symbol\lxTableColumnHead{} & Pronounciation\lxTableColumnHead{} & Meaning\lxTableColumnHead{} & ASCII equivalent\lxTableColumnHead{}\\ | ||
\hline\lxEndTableHead | ||
$\enot$ & not sign & logical not & \verb+~+ or \verb+-+\\ | ||
$\eor$ & or & logical or & \verb+\/+\\ | ||
$\eand$ & and & logical and & \verb+/\+ or \verb+&+\\ | ||
$\eif$ & right arrow & conditional & \verb+->+ or \verb+>+\\ | ||
$\eiff$ & left right arrow & biconditional & \verb+<->+ or \verb+<>+\\ | ||
$\ered$ & up tack & contradiction & \verb+_|_+ or \verb+!?+\\ | ||
$\forall$ & for all & universal quantifier & \verb|A| or \verb|@|\\ | ||
$\exists$ & there exists & existential quantifier & \verb|E| or \verb|3|\\ | ||
$\therefore$ & therefore & therefore & \verb|:.|\\ | ||
$\proves$ & right tack & proves & \verb+|-+\\ | ||
$\nproves$ & does not prove & does not prove & \verb+|/-+\\ | ||
$\entails$ & true & entails & \verb+|=+\\ | ||
$\nentails$ & not true & does not entail & \verb+|/=+\\ | ||
$\ebox$ & white square & necessary & \verb+[]+\\ | ||
$\ediamond$ & white diamond & possible & \verb+<>+ | ||
\end{tabular} | ||
|
||
Subscripts should be pronounced by screen readers, although | ||
if the subscript is a number, they may not be. They can be | ||
represented by an underline, e.g., $A_2$ as \verb|A_2|. | ||
|
||
The expressions `\blank{}' and `\ifeff' are used throughout the textbook. | ||
`Iff' is short for `if and only if'. The HTML versions of both are | ||
provided with ARIA labels to help screen readers pronounce them | ||
properly (i.e., as `blank' and `if-eff'). | ||
|
||
\paragraph{Proofs} The natural deduction proofs in | ||
\cref{ch.NDTFL,ch.NDFOL,Proof} use vertical lines to indicate where | ||
subproofs start and end. Such vertical lines extend from the | ||
assumption line of the subproof to its last line and are displayed | ||
between the line numbers and the formulas in any given line. This | ||
makes proofs a special challenge for blind users. | ||
|
||
To make these proofs accessible in this HTML version, proofs are coded | ||
as tables. Each table line has four columns: the line number, a | ||
subproof level indicator, a formula, and a justification. The subproof | ||
level indicator is a number recording how many nested subproofs the | ||
current line is contained in. It is 0 if the line is not contained in | ||
a subproof, 1 if it is in a subproof, 2 if it is in a subproof nested | ||
within another subproof, and so on. When reading out a subproof level | ||
indicator, screen readers should also announce if a subproof has just | ||
been closed on the previous line, and when a new subproof starts. The | ||
table header rows and subproof level indicators are hidden so that | ||
proofs visually appear as in the printed text. | ||
|
||
Here is an example of such a proof: | ||
\begin{fitchproof} | ||
\hypo{wxyz}{(W \eor X) \eor (Y \eor Z)}\PR | ||
\hypo{xy}{X \eif Y}\PR | ||
\hypo{nz}{\enot Z}\PR | ||
\open | ||
\hypo{wx}{W \eor X}\AS | ||
\open | ||
\hypo{w}{W}\AS | ||
\have{wy1}{W \eor Y}\oi{w} | ||
\close | ||
\open | ||
\hypo{x}{X}\AS | ||
\have{y1}{Y}\ce{xy, x} | ||
\have{wy2}{W \eor Y}\oi{y1} | ||
\close | ||
\have{wy3}{W \eor Y}\oe{wx, w-wy1, x-wy2} | ||
\close | ||
\open | ||
\hypo{yz}{Y \eor Z}\AS | ||
\have{y}{Y}\ds{yz, nz} | ||
\have{wy}{W \eor Y}\oi{y} | ||
\close | ||
\have{wy4}{W \eor Y}\oe{wxyz, wx-wy3, yz-wy} | ||
\end{fitchproof} | ||
It has 14 lines, with 3 premises, 2 levels of subproof nesting, and | ||
two pairs of adjacent subproofs. For instance, the subproof beginning | ||
on line 5 ends at line 6, and line 7 starts another subproof. So the | ||
subproof levels of lines 6 and 7 is the same, but lines 6 and 7 are in | ||
different subproofs. If you cannot see the subproof lines, you have to | ||
pay special attention to how the subproof level numbers change | ||
\emph{and} when a formula is an assumption. A screen reader should | ||
announce line 7 as ``7, close subproof, 2, open subproof, $X$, | ||
Assumption.'' | ||
|
||
\end{document} |