MATHEMATICS

Views include:

Arithmetic/Algebra

High level

Overview

Associations

Universities

Logic

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

Proof assistants

Process calculus

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 refers to the propositional (or boolean) satisfiability problem. 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.

FOL and predicate logic

Subjective logic

Deontic logic

Other

Number theory

Primes

Transformations

DSP - FFT - wavelets - compression

Matrices

Information and computation

Tools