MATHEMATICS

Views include:

High level

Overview

Associations

Universities

Mathematics Subject Classification

Problem hardness

Arithmetic and Algebra

Arithmetic is the study of the properties of the traditional operations on numbers—addition, subtraction, multiplication, division, exponentiation, and extraction of roots. In the 19th century, Italian mathematician Giuseppe Peano formalized arithmetic with his Peano axioms, which are important to the field of mathematical logic today.

Algebra is the study of variables and the rules for manipulating these variables in formulas; it is a unifying thread of almost all of mathematics.

Algebra began with computations similar to those of arithmetic, with letters standing for numbers. This allowed proofs of properties that are true no matter which numbers are involved. For example, in the quadratic equation ax^{2}+bx+c=0, where a, b, c can be any numbers whatsoever (except that a cannot be 0 and the quadratic formula can be used to quickly and easily find the values of the unknown quantity x which satisfy the equation. That is to say, to find all the solutions of the equation.

Logic

Reasoning

Intro and overview

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

Tools

Overview

Alloy

Alloy = logic + language + analysis, where Focused on software engineering

Proof assistants

Isabelle (Cambridge/Muenchen)

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.

Process calculus

Finite State Machines

Proposition logic, SAT, SMT

In mathematical logic, satisfiability and validity are elementary concepts of semantics.

SAT

SAT refers to the propositional (or boolean) satisfiability problem.

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.

FOL and predicate logic

Basics

Prolog

KIF

Subjective logic

Deontic logic

Other

Number theory

Primes

Graphs

Intro

Graph in ZK

Transformations

DSP - FFT - wavelets - compression

Matrices

Information and computation

Linear Programming

Tools

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.