- Views - numbers, shapes, calculus, reasoning, ...
- High level overviews
- Associations
- Universities
- Logic
- Process calculus
- Finite State Machines
- Proposition logic - SMT, SAT
- FOL
- Subjective logic
- Deontic logic
- Number theory
- Transformations
- Information and computation
- Tools

- 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 (...)

- classic
- modern/linear
- abstract algebra (how to specify sets, groups, rings, fields, how to compute with their elements)
- Abstract Algebra - great overview + Sage exercises

- Karl Popper -
- 'The logic of scientific discovery'
- Also: 'We should therefore claim, in the name of tolerance, the right not to tolerate the intolerant.'

- Tricki – a Wiki-style site that is intended to develop into a large store of useful mathematical problem-solving techniques
- US NIST DLMF - Digital Library of Mathematical Functions
- US NIST DADS - Dictionary of Algorithms and Data Structures
- Encyclopedia-of-math (Springer, in cooperation with the European Mathematical Society)
- European Mathematical Society
- zbMath (Zentralblatt MATH) - books, authors, classification, (related to European Mathematical Society)
- Wikipedia - Mathematics portal

- UK - Royal Society - journals/collections/books eg Newton
- EU - EMIS - European Mathemathical Information Service
- US - MAA
- US - AMS

- Be - Ugent
- Be - KU-Leuven
- DE - Mannheim
- NL - EIDMA - Euler Institute for Discrete Mathematics and its Applications - Henk van Tilborg, Lenstra, ...
- US - Number Theory Web
- US - Berkeley Math
- US - Stanford - Statistics
- IL - Haifa - robotics
- IL - Weizmann
- IL - Weizmann's links to Ben-Gurion, Technion, Haifa, ...

- 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.

- Alonzo Church - Princeton - lambda calculus - Church-Turing
- Saul Kripke - modal logic, Kripke systems
- Michael Huth
- Alessandro Artale - Modelling - DL
- Peter Smith - logic, Gödel, LaTeX, ... (Cambridge)
- ASP- Answer Set Programming (ref Victor Witold Marek)
- Victor Witold Marek- Logic

- Wikipedia - set theory- started by George Cantor
- Stanford on set theory
- Stanford on Zermelo-Fraenkel set theory
- Jonathan Jacky - author of The Way of Z
- Jonathan Jacky - Z examples in LaTeX
- Z user group

- 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

- Formal verification software- overview by David Mentré - legacy

- 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

- 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

- 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-
- 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

- Pi calculus- a process calculus
- Process calculus - e.g. Hoare CSP

- 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

- 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.

- Satisfiability.org- conference on propositional satisfiability problem (SAT)
- Satlib- benchmark problems, solvers and tools for SAT research

- 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- Wikipedia
- Predicate calculus, at the Encyclopedia of Mathematics
- Tree Proof Generator (Semantic Tableaux) for propositional or predicate logic, with documentation
- SWISH - SWI-Prolog, with notebooks
- SWISH - SWI-Prolog for the Semantic Web, e.g. handling triples
- Learn Prolog Now , Blackburn, Bos and Striegnitz 2001

- Audun Josan - probabilistic, beliefs-based

- Stanford - Deontic Logic - addressing what is (im)permissible, obligatory, etc

- GOLD parser eg for BNF

- Computational Group Theory - GAP language
- www.combinatorics.org
- www.openscience.org - includes math
- MathFAQ
- UK Turnbull - School for Math and Computational Science - MacTutor - History of Mathematics Archive
- Glossary of Mathematical Mistakes -
*one of the funny sides of math*

- 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