# MATHEMATICS

## Views include:

• Arithmetic (Egypt - numbers), geometry (Greece - shape), calculus (Europe - 17th century - motion, change, space).
• Counting (arithmetic - number theory - primes), reasoning and communication (logic, Venn diagrams, set theory, grammar), motion and change (series, functions, calculus, differentials, integration, analytic number theory), shape (geometry), symmetry (symmetry groups, sphere packing), position (topology, surfaces, knots, elliptic curves)
• mathematica (...)

### Arithmetic/Algebra

• classic
• modern/linear
• abstract algebra (how to specify sets, groups, rings, fields, how to compute with their elements)

# Logic

## Reasoning

• Inductive reasoning
• A method of reasoning in which the premises are viewed as supplying some evidence, but not full assurance, of the truth of the conclusion.
• It is also described as a method where one's experiences and observations, including what are learned from others, are synthesized to come up with a general truth.
• Many dictionaries define inductive reasoning as the derivation of general principles from specific observations (arguing from specific to general), although there are many inductive arguments that do not have that form
• Conclusions from inductive reasoning are probably, not certain
• Deductive reasoning
• Is the process of reasoning from one or more statements (premises) to reach a logical conclusion.
• Deductive reasoning links premises with conclusions.
• If all premises are true, the terms are clear, and the rules of deductive logic are followed, then the conclusion reached is necessarily true.

## Set theory and Z

### Intro

The formal specification notation Z is based on Zermelo-Fraenkel set theory and first order predicate logic. It has been developed by the Programming Research Group at the Oxford University Computing Laboratory and elsewhere since the late 1970s, inspired by Jean-Raymond Abrial's seminal work. Z is now defined by the ISO/IEC 13568 standard and is public domain.

### Z tools

• CZT - Community Z Tools, including LaTeX styles and parsers, typecheckers, etc
• czt-ide - Releases of standalone CZT IDE, based on Eclipse platform. Use it to author, develop and verify Z specifications.
• czt-ide-updates - Update sites for released CZT Eclipse plugins to be installed in your own Eclipse IDE.
• czt-jedit - Plugins for the jEdit text editor (www.jedit.org) adding support for typesetting Z specifications.
• czt - Standalone CZT library (classic distribution).
• maven - Instructions how to use CZT libraries deployed to Maven Central.
• CZT Z/Eves- Z Eclipse automated theorem prover IDE
• ZTC- Z type checker
• HOL-Z- High Order Logic Z checker - a plug-in for Isabelle/HOL

## Tools

### Alloy

Alloy = logic + language + analysis, where
• logic = first order logic + relational calculus
• language = syntax for structuring specifications in the logic
• analysis = bounded exhaustive search for counterexample to a claimed property using SAT
Focused on software engineering
• Alloy- MIT website, from Daniel Jackson
• Alloytools - for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks

### Proof assistants

#### Isabelle (Cambridge/Muenchen)

• Isabelle- generic proof assistant, allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus, originally developed at the University of Cambridge and Technische Universität Muenchen
• Isabelle- University of Cambridge website
• Isabelle- Concrete Semantics (how to)

#### Coq (INRIA)

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, the Verified Software Toolchain for verification of C programs, or the Iris framework for concurrent separation logic), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem, or homotopy type theory), and teaching.
• Coq-
• Coq implements a program specification and mathematical higher-level language called Gallina, based on a formal language called the Calculus of Inductive Constructions that itself combines both a higher-order logic and a richly-typed functional programming language

## Finite State Machines

• FSM - Wikipedia
• NuSMV- Nex Symbolic Model Checker - open source SAT solver for Temporal Logic such as LTL and CTL - a reimplementation and extension of SMV symbolic model checker

## Proposition logic, SAT, SMT

In mathematical logic, satisfiability and validity are elementary concepts of semantics.
• A formula is satisfiable if it is possible to find an interpretation (model) that makes the formula true.
• A formula is valid if all interpretations make the formula true.

### SAT

SAT refers to the propositional (or boolean) satisfiability problem.
• Satisfiability.org- conference on propositional satisfiability problem (SAT)
• Satlib- benchmark problems, solvers and tools for SAT research

### SMT

Satisfiability Modulo Theories (SMT) is an area of automated deduction that studies methods for checking the satisfiability of first-order formulas with respect to some logical theory T of interest. It differs from general automated deduction in that the background theory T need not be finitely or even first-order axiomatizable, and specialized inference methods are used for each theory.
• By being theory-specific and restricting their language to certain classes of formulas (such as, typically but not exclusively, quantifier-free formulas), these specialized methods can be implemented in solvers that are more efficient in practice than general-purpose theorem provers.
• An SMT instance is a formula in first-order logic, where some function and predicate symbols have additional interpretations, and SMT is the problem of determining whether such a formula is satisfiable.
• SMT - Wikipedia
• SMTLIB- the Satisfiability Module Theories library
• Z3- Satisfiability Modulo Theories (SMT) solver by Microsoft

# Tools

• NIST DADS - Dictionary of Algorithms and Data Structures - includes definitions such as NP etc, as well as algorithms and datastructures
• NIST GAMS - Guide to available mathematical software - including problem taxonomy
• imaginary.org- education and open source
• iPhython.org
• regex - a regular expression is a sequence of characters that define a search pattern
• A regex processor translates a regular expression into an internal representation which can be executed and matched against a string representing the text being searched in.
• Each character in a regular expression is either a metacharacter or a regular character that has a literal meaning. For example, in the regex a., a is a literal character which matches just 'a', while '.' is a metacharacter that matches every character except a newline.
• Basics:
• a matches letter 'a'
• [a-z] matches all lower case letters from 'a' to 'z'
• '.' is a metacharacter that matches every character except a newline
• a vertical bar separates alternatives ('or'), e.g. gr(a|e)y
• Quantifiers: a quantifier after a token (such as a character) or group specifies how often that a preceding element is allowed to occur
• ? indicates zero or one occurrences of the preceding element. For example, colou?r matches both "color" and "colour".
• * indicates zero or more occurrences of the preceding element. For example, ab*c matches "ac", "abc", "abbc", "abbbc", and so on.
• + indicates one or more occurrences of the preceding element. For example, ab+c matches "abc", "abbc", "abbbc", and so on, but not "ac"
• {n} means the preceding item is matched exactly n times.
• Anchors:
• ^The matches any string that starts with The
• end\$ matches a string that ends with end
• ^The end\$ exact string match (starts and ends with The end)
• roar matches any string that has the text roar in it
• Character classes:
• \d matches a single character that is a digit
• \w matches a word character (alphanumeric character plus underscore)
• \s matches a whitespace character (includes tabs and line breaks)
• \d, \w and \s also present their negations with \D, \W and \S respectively, for example, \D will perform the inverse match with respect to that obtained with \d, so \D matches a single non-digit character
• . matches any character as a wildcard, for example, a.b matches any string that contains an "a", then any other character and then a "b", a.*b matches any string that contains an "a" and a "b" at some later point.
• Escaping: in order to be taken literally, you must escape the characters ^.[\$()|*+?{\with a backslash \ as they have special meaning, e.g. \\$\d matches a string that has a \$ before one digit
• Non-printables: you can match also non-printable characters like tabs \t, new-lines \n, carriage returns \r
• Using \1 to keep part of the pattern: "[a-z][a-z]" will match any two lower case letters. If you wanted to search for lines that had two adjoining identical letters, this pattern wouldn't help. You need to remember what you found, and see if the same pattern occurred again.
• To mark part of a pattern using "\(" and "\)",
• To recall the remembered pattern use "\" followed by a single digit.
• Therefore, to search for two identical letters, use "\([a-z]\)\1". You can have 9 different remembered patterns.
• Standards: the IEEE POSIX standard has 3 sets of compliance: BRE (Basic Regular Expressions), ERE (Extended Regular Expressions), and SRE (Simple Regular Expressions) - deprecated
• Regex can be used e.g. in grep or sed, such as 'sed 's/regexp/replacement/g' inputFileName > outputFileName'
• In sed the s stands for substitute, while the g stands for global, which means that all matching occurrences in the line would be replaced.
• The replacement can be literal text or a format string containing the characters & for "entire match" or the special escape sequences \1 through \9 for the nth saved sub-expression
• Regex editor e.g. any https corresponds to /[https\:\/\/]/

• sed - gnu.org page
• sed - wikipedia - basic examples
• Usage: sed SCRIPT INPUTFILE...
• Usage for substitution: sed 's/regexp/replacement/g' inputFileName > outputFileName where
• s represents the substitute command
• g represents the global flag, i.e. replace all occurances found, not only the first one (as by default)
• ...

• SageMath.org - OpenSource Mathematica
• SageMath expository from David Joyner
• SageMath - William Stein
• SageMath Wiki
• Wolfram's MATHworld - Eric Weisstein's World of Mathematics
• Wolfram's Mathematica
• Wolfram's search engine/solver - Wolfram Alpha
• MathWorks - MATLAB -
• NL - The MathWorks - MATLAB & Toolboxes such as:
• Statistic
• Curve Fitting
• Optimization
• Symbolic Math
• Image Processing
• Signal Processing
• Neural Network
• Filter Design

### Humour

When a statistician passes the airport security check, they discover a bomb in his bag. He explains. "Statistics shows that the probability of a bomb being on an airplane is 1/1000. However, the chance that there are two bombs at one plane is 1/1000000. So, I am much safer..."

The same statistician later drowned in a river with an average depth of 30 cm.