MATHEMATICS

Views include:

Arithmetic/Algebra

High level

Overview

Associations

Universities

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

Subjective logic

Deontic logic

Other

Number theory

Primes

Transformations

DSP - FFT - wavelets - compression

Matrices

Information and computation

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.