MATHEMATICS
- Views and branches - numbers, shapes, arithmethic, calculus, reasoning, ...
- High level overviews
- Associations
- Universities
- Problem hardness and complexity
- Famous solved problems
- Proofs
- Arithmetic - modular arithmethic, p-adic numbers
- Algebra - set, group, ring, field, polynomial, elliptic curve, pairing, ...
- Logic
- Process calculus
- Finite State Machines
- Proposition logic - SMT, SAT
- FOL
- Subjective logic
- Deontic logic
- Number theory
- Graphs
- Transformations
- Linear Programming
- Information and computation
- Tools
- Humour
Views and branches
Views
- 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 (...)
Branches of abstract algebra
- Abstract algebra (how to specify sets, groups, rings, fields, how to compute with their elements)
- Abstract Algebra - great overview + Sage exercises, covering:
- The Integers
- Groups
- Cyclic Groups
- Permutation Groups
- Cosets and Lagrange’s Theorem
- Introduction to Cryptography
- Algebraic Coding Theory
- Isomorphisms
- Normal Subgroups and Factor Groups
- Homomorphisms
- Matrix Groups and Symmetry
- The Structure of Groups
- Group Actions
- The Sylow Theorems
- Rings
- Polynomials
- Integral Domains
- Lattices and Boolean Algebras
- Vector Spaces
- Fields
- Finite Fields
- Galois Theory
High level
Overview
Associations
Universities
Mathematics Subject Classification
Problem hardness and complexity
P, NP, NP-complete, NP-hard
- P versus NP - Wikipedia
- The P versus NP problem is a major unsolved problem in theoretical computer science. In informal terms, it asks whether every problem whose solution can be quickly verified can also be quickly solved.
A language L is in NP if for every word x in the language there exists a witness w which is of length polynomial in the length of x and given the witness and the word you can verify language-membership in polynomial time.
Note that you only need said witness (sometimes also called certificate) need only exist for words that actually are in the language, i.e. you don't need to be able to construct them for negative instances and constructing them is allowed to take super-polynomial time.
P for Polynomial time
- Polynomial time - Wikipedia
- An algorithm is said to be of polynomial time if its running time is upper bounded by a polynomial expression in the size of the input for the algorithm, that is, T(n) = O(n^k) for some positive constant k.
- Problems for which a deterministic polynomial-time algorithm exists belong to the complexity class P.
- Cobham's thesis states that polynomial time is a synonym for "tractable", "feasible", "efficient", or "fast".
NP for Non-deterministic Polynomial time
- Non-deterministic Polynomial time - Wikipedia
- Have proofs verifiable in polynomial time.
- It is easy to see that the complexity class P (all problems solvable, deterministically, in polynomial time) is contained in NP (problems where solutions can be verified in polynomial time), because if a problem is solvable in polynomial time, then a solution is also verifiable in polynomial time by simply solving the problem.
- NP-completeness - short for "nondeterministic polynomial-time complete - Wikipedia
- Although a solution to an NP-complete problem can be verified "quickly", there is no known way to find a solution quickly.
- NP-hardness - short for "nondeterministic polynomial-time complete - Wikipedia
- is the defining property of a class of problems that are informally "at least as hard as the hardest problems in NP".
- A simple example of an NP-hard problem is the subset sum problem.
- Subset Sum Problem - Wikipedia
- There is a multiset S of integers and a target-sum T, and the question is to decide whether any subset of the integers sum to precisely T.
- The problem is known to be NP-hard. Moreover, some restricted variants of it are NP-complete.
Computational complexity
Time complexity
- Time complexity - Wikipedia
- Describes the amount of computer time it takes to run an algorithm.
- Commonly estimated by counting the number of elementary operations performed by the algorithm, supposing that each elementary operation takes a fixed amount of time to perform.
- Thus, the amount of time taken and the number of elementary operations performed by the algorithm are taken to be related by a constant factor.
- Since an algorithm's running time may vary among different inputs of the same size, one commonly considers the worst-case time complexity, which is the maximum amount of time required for inputs of a given size.
To express the running time of an algorithm one can use a combination of two ideas.
- One needs to determine how long the algorithm takes, in terms of the size of its input.
- Also, one needs to consider how fast a function grows with the input size, the rate of growth of the running time.
Suppose an algorithm, running on an input of size n takes 6n2+100n+300 machine instructions.
This expression is a polynomial with n as variable (indeterminate).
The 6n2 squared term becomes larger than the remaining terms, 100n+300 once n becomes large enough, 20 in this case.
The running time of this algorithm is specified as n2 dropping the coefficient 6 and the remaining terms 100n+300.
The less significant terms and the constant coefficients are dropped to focus on the important part of an algorithm's running time—its rate of growth—without getting mired in details.
This is called 'asymptotic notation', of which there are the following forms.
- Asymptotic notation - Khan Academy
- big-Θ (big-theta) notation expresses that a running time, once n gets large enough, the running time is at least k1⋅n and at most k2⋅n for some constants k1 and k2.
- big-Ω (big-omega) notation expresses that an algorithm takes at least a certain amount of time, without providing an upper bound.
- Big-Ω notation is used for asymptotic lower bounds, it bounds the growth of the running time from below for large enough input sizes.
- big-O notation, typically O(n), O(log n), O(n^a), etc., where n is the size in units of bits needed to represent the input.
- Algorithmic complexities can be classified according to the type of function appearing in the big O notation. For example, an algorithm with time complexity O(n) is a linear time algorithm and an algorithm with time complexity O(n^a) for some constant a > 1 is a polynomial time algorithm.
- Big O notation - Wikipedia
Circuit complexity
- Circuit complexity - Wikipedia
- branch of computational complexity theory in which Boolean functions are classified according to the size or depth of the Boolean circuits that compute them.
- A related notion is the circuit complexity of a recursive language that is decided by a uniform family of circuits
Famous solved problems
Proofs
Basics
- Proof - an overloaded term - Wikipedia
- Propositional proof - 'truth' - Wikipedia
- Formal proof - Wikipedia - a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference.
- Proof complexity - Wikipedia - concerned with proving proof-length lower and upper bounds in various propositional proof systems - connects to SAT solvers
Soundness and completeness
In mathematical logic, logical systems are sound if and only if every formula that can be proved in the system is logically valid with respect to the semantics of the system.
The converse of soundness is known as completeness.
A formal system is called complete with respect to a particular property if every formula having the property can be derived using that system, i.e. is one of its theorems; otherwise the system is said to be incomplete.
Interactive Proofs
In 'A paradoxial solution to the signature problem' Goldwasser, Micali and Rivest specify that the standard definition of interactive proofs require
- that the verifier accepts a correct proof, and
- rejects an incorrect assertion with a probability of at least 2/3.
- ... however, one usually tries to obtain a probability less than 2-k where k is the security parameter...
- ...a way to achieve this 'security amplification' is to take a protocol with 1/3 error probability, run it O(k) times and accept/reject by majority vote
Probabilistically Checkable Proofs (PCP)
Used a.o. in SNARKS.
- PCP - Wikipedia
- A type of proof that can be checked by a randomized algorithm using a bounded amount of randomness and reading a bounded number of bits of the proof. The algorithm is then required to accept correct proofs and reject incorrect proofs with very high probability.
- A standard proof (or certificate), as used in the verifier-based definition of the complexity class NP, also satisfies these requirements, since the checking procedure deterministically reads the whole proof, always accepts correct proofs and rejects incorrect proofs.
- However, what makes them interesting is the existence of probabilistically checkable proofs that can be checked by reading only a few bits of the proof using randomness in an essential way.
Arithmetic
Arithmethic
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.
Modular arithmetic
- Modular arithmetic developed by Carl Friedrich Gauss in his book Disquisitiones Arithmeticae, 1801
- Given an integer n > 1, called a modulus, two integers a and b are said to be congruent modulo n, if n is a divisor of their difference (that is, if there is an integer k such that a − b = kn).
- The modulo operation: the notation b mod n (without parentheses) refers to the modulo operation. Indeed, b mod n denotes the unique integer a such that 0 ≤ a < n and a ≡ b (mod n)(that is, the remainder of b when divided by n
- The congruence equation: the notation a ≡ b (mod n), where the parentheses mean that (mod n) applies to the entire equation, not just to the right-hand side (here, b).
- Given an integer n > 1, called a modulus, a ≡ b (mod n) if n is a divisor of their difference (if there is an integer k such that a − b = k.n)
- Reduction: 9 (mod 2) ≡ 1 (mod 2) (there is an integer k(=4) such that 9-1 = k.2
- Reduction: 9 (mod 2) ≡ 1 (mod 2) (there is an integer k(=4) such that 9-1 = k.2
- Reduction: 8 (mod 2) ≡ 0 (mod 2) (there is an integer k(=4) such that 8-0 = k.2
- Planetcalc - all kinds of calculators including for modular arithmethic
- Observation: 7-5=2, 5-7=-2 7 ≡ 5 (mod 2) because 7-5=2, (2 mod 2) = -4 | 2
- In modulus 12, one can assert that 38 ≡ 14 (mod 12) because 38 − 14 = 24 (a multiple of 12, with k=2). Alternatively, 14 ≡ 38 (mod 12) because 14 − 38 = -24 (also a multiple of 12, with k=-2).
- Another way to express this is to say that both 38 and 14 have the same remainder 2, when divided by 12.
- More examples: 8 mod 4 ≡ 0, 7 mod 2 ≡ 1
- The definition of congruence also applies to negative values. For example:
- 2 ≡ − 3 (mod 5) because -3 -2 | 5 (the notation (mod 5) at the end of the expression means mod 5 applies to both sides of the equation)
- − 8 ≡ 7 (mod 5) because 7 - (-8) = 15 | 5
- − 3 ≡ − 8 (mod 5) because -8 - (-3) = 5 | 5
- 1 ≡ − 3 (mod 2) because -3 -1 = -4 | 2
- 330 ≡ -1 (mod 331) because -1 - 330 = -331 | 331
- Fermat's little theorem and quite a few other calculators
- If p is a prime number, then for any integer a, the number ap − a is an integer multiple of p.
- Expressed otherwise: ap ≡ a mod p
- Also, if a is not divisible by p, Fermat's little theorem is equivalent to the statement that ap − 1− 1 is an integer multiple of p.
- Expressed otherwise: ap-1 ≡ 1 mod p
- Root of unity modulo n - Wikipedia and quite a few other calculators
- A kth root of unity modulo n for positive integers k, n ≥ 2, is a root of unity in the ring of integers modulo n; that is, a solution x to the equation (or congruence) x k ≡ 1 ( mod n ).
- If k is the smallest such exponent for x, then x is called a primitive kth root of unity modulo n.
- Modular arithmetic calculator and quite a few other calculators
p-adic numbers
- p-adic number - Wikipedia
- the p-adic number system for any prime number p extends the ordinary arithmetic of the rational numbers in a different way from the extension of the rational number system to the real and complex number systems.
- The extension is achieved by an alternative interpretation of the concept of "closeness" or absolute value. In particular, two p-adic numbers are considered to be close when their difference is divisible by a high power of p: the higher the power, the closer they are.
- This property enables p-adic numbers to encode congruence information in a way that turns out to have powerful applications in number theory – including, for example, in the famous proof of Fermat's Last Theorem by Andrew Wiles
- p-adic valuation - Wikipedia
- the p-adic valuation or p-adic order of an integer n is the exponent of the highest power of the prime number p that divides n. It is denoted νp(n) Equivalently, νp(n) is the exponent to which p in the prime factorization of n.
Algebra
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. Many areas of mathematics belong to algebra, some having "algebra" in their name, such as commutative algebra, and some not, such as Galois theory.
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.
- Algebra - Wikipedia
- Elementary algebra deals with the manipulation of variables such as x as if they were numbers.
- Linear algebra, which deals with linear equations and linear mappings, is used for modern presentations of geometry, and has many practical applications (weather forecasting ...).
- Abstract algebra is the name given to the study of algebraic structures such as groups, rings, and fields, see below
- Abstract Algebra - great overview + Sage exercises
Abstract algebra
Sets and cosets
Groups
- Group - is a set and an operation that combines any two elements of the set to produce a third element of the set, in such a way that the operation is associative, an identity element exists and every element has an inverse
- Otherwise said: Group G is a set with 1 binary operation * such that following properties holds: * is associative, there is an identity element, each element has an inverse element
- If a * b = b * a then the group is called abelian or commutative
- If there exists a generator g such that for any element b there is an integer j such that gj = b then the group is cyclic
- The number of elements in a finite group is called its order, |G|
- The subgroup of G consisting of all powers of the element a is called the subgroup generated by a, denoted by bracket a bracket
- And bracket a bracket is of finite order k if is k is the least positive integer such that ak = e, the identity element
- Example: the integers together with the addition operation form a group.
Rings
- Ring R - set with 2 binary operations (+ and *) such that R is abelian with respect to +, * is associative, and + and * are distributive
- If there is a multiplicative identity the ring is called a ring with identity
- A ring is called commutative if * is commutative
- A ring is called an integral domain if it is a commutative ring with identiy e ¬ = 0 in which ab=0 implies a=0 or b=0
- A ring is called a diision ring if the nonzero elemnts form a group under *
- A commutative division ring is called a field
- Example: the four common rings: the integers Zn, the rationals, the reals, the complex numbers
Fields
Basics
- Set F with 2 binary operations (+ and *)
- Has two distinguished elements: zero element 0 and identity element e such that e ¬ = 0
- Is an abelian group with regard to + with 0 as identity element
- The elements of F that are ¬ = 0 form an abelian group with regard to *, with e as identity element
- The distributive laws hold on + and *
- Example: Zp is a finite field, Zp = {0,1,...,p-1}
Roots
- Root of unity - Wikipedia
- Any complex number that yields 1 when raised to some positive integer power n.
- Can be defined in any field.
- If the characteristic of the field is zero, the roots are complex numbers that are also algebraic integers.
- The characteristic of a ring R, often denoted char(R), is defined to be the smallest number of times one must use the ring's multiplicative identity (1) in a sum to get the additive identity (0). If this sum never reaches the additive identity the ring is said to have characteristic zero.
- For fields with a positive characteristic, the roots belong to a finite field, and, conversely, every nonzero element of a finite field is a root of unity.
- Any algebraically closed field contains exactly n nth roots of unity, except when n is a multiple of the (positive) characteristic of the field.
Quadratic residues, Legendre and Jacobi symbols
QR
- QR - Wikipedia integer q is called a quadratic residue modulo n if it is congruent to a perfect square modulo n; i.e., if there exists an integer x such that x2 ≡ q (mod n) - finding x may be hard
- Euler's criterion - Wikipedia
- Is a formula for determining whether an integer is a quadratic residue modulo a prime via a(p-1)|2 mod p
- Let p be an odd prime and a be an integer coprime to p. Then:
- a(p-1)|2 ≡ 1 mod p if there is an integer x such that a ≡ x2 mod p
- a(p-1)|2 ≡ -1 mod p otherwise
- Illustration 1: which numbers are squares modulo 17 (quadratic residues modulo 17)? We can manually calculate it as:
- 12 = 1
- 22 = 4
- 32 = 9
- 42 = 16
- 52 = 25 ≡ 8 (mod 17)
- 62 = 36 ≡ 2 (mod 17)
- 72 = 49 ≡ 15 (mod 17)
- 82 = 64 ≡ 13 (mod 17).
- So the set of the quadratic residues modulo 17 is {1,2,4,8,9,13,15,16}.
- Illustration 2: let a = 17. For which primes p is 17 a quadratic residue? We can test prime p's manually given the Eurler formula a(p-1)|2 mod p.
- Consider p = 3, then 17(3 − 1)|2 = 171 ≡ 2 ≡ −1 (mod 3), therefore 17 is not a quadratic residue modulo 3.
- Consider p = 13, then 17(13 − 1)|2 = 176 ≡ 1 (mod 13), therefore 17 is a quadratic residue modulo 13. As confirmation, note that 17 ≡ 4 (mod 13), and 22 = 4.
- Law of quadratic reciprocity - Wikipedia
- gives conditions for the solvability of quadratic equations modulo prime numbers
- allows to determine whether there is an integer solution for any quadratic equation of the form x2 ≡ a mod p for an odd prime p, that is, to determine the "perfect squares" modulo p.
Finding a square root of a number modulo a large composite n is equivalent to factoring (which is widely believed to be a hard problem), hence has been used for constructing cryptographic schemes such as the Rabin cryptosystem and the oblivious transfer.
The quadratic residuosity problem is the basis for the Goldwasser-Micali cryptosystem.
Legendre - prime p and integer a
- Legendre symbol - Wikipedia - defined to proof the law of quadratic reciprocity
- Legendre symbol - prime p and integer a
- Let p be an odd prime number. An integer a is a quadratic residue modulo p if it is congruent to a perfect square modulo p and is a quadratic non-residue modulo p otherwise. The Legendre symbol is a function of a and p defined as
- +1 if a is a QR modulo p and a not ≡ 0 mod p
- -1 if a a quadratic non-residue modulo p
- 0 if a is ≡ 0 mod p
Jacobi - [composite] integer n and integer a
- Jacobi symbol integer n and integer a - (generalisation of Legendre) - Wikipedia - usefull a.o. in primality testing and integer factorisation
- Let n be any positive odd integer n (which may be composite). For any integer a, the Jacobi symbol (a/n) is defined as the product of the Legendre symbols corresponding to the prime factors of n
- +1 if a is a QR modulo p and a not ≡ 0 mod p
- -1 if a a quadratic non-residue modulo p
- 0 if a is ≡ 0 mod p
Polynomials
In algebra a polynomial is an expression of the form a0+a1x+...+anxn. The ai are called coefficients (typically real or complex numbers). The x is a variable, substituting an arbitrary number for it a well defined number is obtained.
A polynomial of ring R is a polynomial where the coefficients are element of R, and x is a symbol not belonging to R, called the indeterminate over R.
Addition and product for polynomials over R is defined, and the set of polynomials over R forms a ring, called the polynomial ring over R, R[x]. The highest exponent of n is called the degree of the polynomial.
The prime elements of the ring F[x] are called irreducible polynomials.
Polynomials of postive degree can be uniquely factorised.
An element of a field F is called a root of the polynomial if its value is zero.
In number theory, there's Lagrange's theorem, about how frequently a polynomial over the integers may evaluate to a multiple of a fixed prime.
Elliptic curve
embedding degree k is ...
singular
hyperelliptic
Ways of specifying ECs:
- The traditional way, using the Weierstrass equation: y2= x3+ax+b
- Huff curves,
- Jacobi quartics,
- (twisted) Edwards curves.
EC pairings
Refer also to pairing-based crypto.
NIST: a pairing is a function that maps a pair of points on an elliptic curve into a finite field. Their unique properties have enabled many new cryptographic protocols that had not previously been feasible.
The Weil pairing was first introduced into cryptography by Menezes, Okamoto and Vanstone (A. J. Menezes, T. Okamoto and S. A. Vanstone, Reducing elliptic curve logarithms to logarithms in a finite field, IEEE Trans. Inf. Theory, 39, No. 5 (1993) 1639{1646) to attack the ECDLP on certain elliptic curves.
The Tate pairing was introduced to cryptography by Frey and Rueck (G. Frey and H.-G. Rueck, A remark concerning m-divisibility and the discrete logarithm in the divisor class group of curves, Math. Comp., 62, No.206 (1994) 865{874}) in their extension of the work of Menezes, Okamoto and Vanstone.
Can be calculated with the Miller algorithm.
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.
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
- 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.
- Download archived version for Windows 64 bits
- 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
Overview
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
Process calculus
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
FOL and predicate logic
Basics
Prolog
KIF
- Knowledge Interchange Format - Wikipedia
- Is a computer language designed to enable systems to share and re-use information from knowledge-based systems.
- Similar to frame languages such as KL-One and LOOM but unlike such language its primary role is not intended as a framework for the expression or use of knowledge but rather for the interchange of knowledge between systems.
Has a declarative semantics.Knowledge can be described as objects, functions, relations, and rules.
- It is a formal language, i.e., it can express arbitrary statements in first order logic and can support reasoners that can prove the consistency of a set of KIF statements.
- KIF also supports non-monotonic reasoning.
- Although the original KIF group intended to submit to a formal standards body, that did not occur. A later version called Common Logic has since been developed for submission to ISO and has been approved and published.
- A variant called SUO-KIF is the language in which the Suggested Upper Merged Ontology SUMO) is written.
Subjective logic
Deontic logic
Other
Number theory
Primes
Graphs
Intro
Graph in ZK
DSP - FFT - wavelets - compression
Matrices
Linear Programming
Refer also to LTK and LTK-SageMath.
- 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)
- ...
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.