FMathL - Formal Mathematical Language

FMathL (= Formal Mathematical Language) is the working title for a modeling and documentation language for mathematics, suited to the habits of mathematicians, to be developed in a project at the University of Vienna.

The project complements efforts for formalizing mathematics from the perspective of computer science and automated theorem proving. In the long run, the FMathL system might turn into a user-friendly automatic mathematical assistant for retrieving, editing, and checking mathematics (but also computer science and theoretical physics) in both informal, partially formalized, and completely formalized mathematical form.

The project is part of a greater vision, the creation of an expert system called MathResS ( = Mathematical Research System) that supports mathematicians and scientists dealing with mathematics in a comprehensive way. Part of the project is done in collaboration with the software company DAGOPT.

Related projects by others are MathNat - Mathematical texts in controlled natural language (by Muhammad Humayoun), Naproche - Natural language proof checking (by Marcos Cramer et al., until 2013), A Language for Mathematics (by Mohan Ganesalingam), A Fully Automatic Theorem Prover with Human-Style Output (by Ganesalingam and Gowers), A language for mathematical knowledge management (by Kieffer, Avigad and Friedman), Mathcat (by Akiko Aizawa), and FPL - the Formal Proving Language (by Andreas Piotrowski)


This page is located at http://arnold-neumaier.at/FMathL.html and contains sections on


The FMathL project


FMathL (= Formal Mathematical Language) is the working title for a modeling and documentation language for mathematics, to be developed at the University of Vienna.

If you'd like to be actively involved in the FMathL project, please contact me.

Part of the goals associated with the FMathL language were realized through the project A modeling system for mathematics (MoSMath), supported from 2008-2011 by a grant of the Austrian Science Foundation FWF under contract number P20631.

Another FMathL-related project An automatic mathematical research system (MathResS) never got off the ground, due to lack of funding. All referees in all versions submitted found the project to be far too ambitious to be realizable.

Thus much of what is said here is about plans, some of which is already realized, and some of which will perhaps be realized in the near future.

Most of the content of this web site dates back to 2011. Important additional work was done in 2016-2017.

The design of FMathL is based on our experience with

  • pure and applied mathematics in general,
  • modeling languages,
  • numerical programming systems,
  • test problem collections for various problem types,
  • real applications, and
  • wrong starts in the past.

    The goal of the FMathL project is to combine

  • the universality of the common mathematical language to describe completely arbitrary problems,
  • the advantages of LaTeX for writing and viewing mathematics,
  • the user-friendliness of mathematical modeling systems such as AMPL for the flexible definition of large-scale numerical analysis problems,
  • the high-level discipline of the CVX system for solving convex programming problems and enforcing their semantic correctness, and
  • the semantic clarity of the Z notation for the precise specification of concepts and statements.

    We believe that this goal is reachable, and that an easy-to-use such system will change the way modeling is done in practice. See A modeling system for mathematics for some background information.


    Key characteristics of the future FMathL language

  • separate completely modeling aspects (declarative) and algorithmic aspects (imperative)
  • The model is (almost) a publishing quality documentation; the latter can be automatically generated from the model (cf. Knuth's literate programming paradigm)
  • The formal model is specified close to how it would be communicated informally when describing it in a lecture or paper, except that it does not suppress any relevant detail
  • enables users to express arbitrary mathematics
  • easy exchange of problems in a high level format
  • very transparent use, fully modular
  • user extensible
  • public domain
  • mathematician-friendly: write as in a textbook
  • any mathematical problem can be specified (though not necessarily successfully solved by a solver to which it is passed - some problems are too difficult or even undecidable)
  • prepares the way for an easy-to use formalized mathematics interface covering the contents of undergraduate mathematics courses and beyond
  • later extensions only affect the interfaces, not the problem structure, and can be contributed by third parties


    Specifications in FMathL

  • specify relevant background in mathematics in the way you'd communicate it in a lecture or research paper
  • specify problems in their natural mathematical form, with functions, sets, operators, measures, quantifiers, tables, cases rather than loops, indices, diagrams, etc.
  • specify algorithms by their requirements (input conditions, output conditions) rather than by a piece of pseudo-code
  • specify strategies for combining algorithms to solve problems of a given category
  • specify programs executing an algorithm by semantically well-defined code
  • document which programs satisfy which algorithmic specifications, such that in principle (and perhaps in a follow-up project MathResS) program verification is possible
  • from these specifications, automatically create the structures needed to interface with existing programming systems (LAPACK, Matlab, etc.) and solvers (for optimization problems, ODEs, PDEs, etc.), and with LaTeX for documentation
  • as part of the latter, include automatic differentiation (and other source-transforming) capabilities on the highest level, differentiating specifications rather than codes.


    FMathL project update 2016-2017

    Some of the progress on the project achieved in the last few years is discussed in the following three lactures:

    A. Neumaier, The communication of mathematics, Lecture, Isaac Newton Institute for Mathematical Sciences, Cambridge 2017.
    video of the lecture

    A. Neumaier, Concise - a synthesis of types, grammars, semantics Lecture, Isaac Newton Institute for Mathematical Sciences, Cambridge 2017.
    video of the lecture

    A. Neumaier, From Informal to Formal Mathematics, Slides of a lecture presented at VINO 2017 (Technical University Vienna, Austria)

    These lectures summarize parts of the master thesis by Andreas Pichler and the Ph.D. thesis by Kevin Kofler; see the references below.

    Loosely related to FMathL is my lecture

    A. Neumaier, Artificial Intelligence, Mathematics, and Consciousness, Slides, 2016.

    Important references

    P. Schodl, Foundations for a self-reflective, context-aware semantic representation of mathematical specifications, Ph.D. thesis, Faculty of Mathematics, University of Vienna (2011).

    F. Domes, A. Neumaier, K. Kofler, P. Schodl, H. Schichl, Concise Manual, Version 0.91, Faculty of Mathematics, University of Vienna (2014).

    A. Pichler, Semantische Repräsentation mathematischer Konzepte, Masterarbeit, Faculty of Mathematics, University of Vienna (2016).

    K. Kofler, Dynamic Generalized Parsing and Natural Mathematical Language, Ph.D. thesis, Faculty of Mathematics, University of Vienna (2017).

    DynGenPar - Dynamic Generalized Parser for generalized context free grammars (by Kevin Kofler)
    supports dynamic grammar additions, incremental parsing, prediction, rule labels, custom parse actions, arbitrary token sources, hierarchical parsing, parallel multiple context-free grammars (PMCFGs), and next token constraints.


    Software created by 2012

    Concise, a graph-based universal programming system for manipulating semantic information stored in the semantic memory. It combines in a novel way the capabilities of imperative programming and object-oriented programming. (Online is only an old version with much less capability than described in the thesis by Kevin Kofler.)

    DynGenPar, an innovative parser based on a new principle combining bottom-up and top-down features of traditional parsers. The most unique feature of the algorithm is the possibility to add rules to the grammar at almost any time, even during parsing.

    Papers and technical reports until 2012


    Other results obtained by 2012


    The FMathL mathematical framework

    The FMathL mathematical framework is designed to be a formal framework for mathematics that will allow the convenient use and communication of arbitrary mathematics (including logic) on a computer, in a way close to the actual practice of mathematics.

    Several frameworks for mathematics have been constructed in the literature. To avoid the paradoxes of naive set theory, Zermelo and Fraenkel constructed a type-free system of sets, based on first order predicate logic, while von Neumann, Bernays and Gödel constructed a system with two types, sets and classes. These and related systems suffice for the common needs of a working mathematician. But they are inconvenient to use without pervasive abuse of language and notation, which makes human-machine communication of mathematics difficult. My essay ''Interpreting informal mathematical language'' illustrates some difficulties that need to be overcome, due to different views on how to formalize mathematical statements, and my essay ''Foundations of Mathematics'' discusses some widely differing views on what should be the proper foundations.

    The paper ''Logic in context'' describes the context logic of FMathL, a set-theoretical setting for natural deduction that abstracts the changing contexts in typical mathematical discourse. It is equivalent to the fragment of intuitionistic logic without or (which sufficies for the verification of proof checkers), and augmented by the law of excluded middle gives classical propositional logic. Quantifiers can be handled in this setting via Hilbert's and Bourbaki's global choice operator.

    In contrast to traditional implementations of mathematics in ZFC, combinatory logic, CCAF, or related logical systems, FMathL only formalizes the common (finitist) ground of most mathematicians. This makes FMathL compatible with multiple, possibly conflicting philosophies regarding the meaning of terms outside their intended use.

    On the other hand, we also work towards a possible foundation that captures as valid features the many familiar abuses of language and terminology that are unavoidable when pressing mathematics as practiced into one of the foundational systems that exist. The current syntax-free, abstract level of a first trial version of an FMathL mathematical framework; will be replaced in the future by one that is much less demanding in its assumptions, so that work for a wider audience.

    In the FMathL mathematical framework, all axioms are given in the form of familiar existence requirements and properties that are used by mathematicians on an everyday basis. Typical mathematicians (those trusting the axiom of choice and hence the law of excluded middle) can readily convince themselves of their truth in their private (but publicly educated) view of mathematical concepts. The exposition is such that students exposed to the typical introductory mathematics courses should have no serious difficulty understanding the material.

    See also:

    How to write a nice, fully formalized proof
    This is a piece of output of a current proof assistant, and a translation showing how a mathematician would write down the same information. The example shows that formal mathematics need not look like an indigestible mess of low level proof information.

    Towards a Computer-Aided System for Real Mathematics (an extended thread in the n-Category Cafe, related to FMathL and categorial foundations of mathematics)


    MoSMath

    A modeling system for mathematics (MoSMath)
    The scientific proposal for the part of the project funded by the Austrian Science foundation FWF

    Slides of a lecture on MoSMath by Peter Schodl, at the Seminar Formale Mathematik of the Naproche project

    SMPL - A Simplified Modeling Language for Mathematical Programming
    A simple, AMPL-like modeling language for posing constraint satisfaction problems and global optimization problems


    The FMathL type system

    In the paper The FMathL type system, we formally define a framework for representing semantic content, specially designed to naturally represent arbitrary mathematics. Information is represented via semantic units (sems) relating nodes, an undefined notion that may be interpreted as entries in a semantic matrix, as elements of the domain of a semantic mapping, or as vertices and edges of a semantic graph.
    Information can be typed, and types can be declared. The FMathL type system is a common generalization of both (certain) polymorphic types in programming languages and (context-free) grammatical categories in linguistics. The type declaration themselves are represented via typed nodes, making the whole typing self-consistent. Correctness of types can be checked in linear time. A context free grammar for the specification of types is described, and examples are given, including the representation of many diverse mathematical expressions.

    Two sample type sheets, one for the type system and one for optimization problems from the OR Library, illustrate the way specific type structures are created.

    In the paper Representing expressions in the semantic memory, we show how a large variety of expressions (enough to cover common mathematical syntax, and easily extensible to cover more specialized notation) can be represented in the semantic memory.


    Concise - The FMathL integrated development environment

    To support the development of FMathL, we created a Java programming environment called Concise. Concise is intended for user-friendly data entering and manipulation, algorithm design and execution, and more general for interaction with the semantic memory. Concise has configurable display and text completion. A first public (alpha) version is available, but much of its functionality is still too low level for real applications.

    A first proof-of-concept application to the semantic representation of mathematical concepts is given in Semantische Repräsentation mathematischer Konzepte (pdf file, 1080K, by Andreas Pichler)

    For more on the current functionality of Concise see
    K. Kofler, Dynamic Generalized Parsing and Natural Mathematical Language, Ph.D. thesis, Faculty of Mathematics, University of Vienna (2017).


    ALA

    We are planning to work towards a formal version of standard undergraduate courses on analysis and linear algebra, to have a basis for doing more advanced formal mathematics.
    The planned database will at least contain formalized statements of all results stated and proved in the following lecture notes on analysis and linear algebra (ALA):

    Analysis und lineare Algebra
    by Arnold Neumaier
    Lecture Notes in German (456pp.)
    It contains 23 chapters with standard undergraduate mathematics,

  • starting with naive set theory, groups, rings, and fields, and an axiomatic definition of the complex numbers,
  • covering (among many other things) standard linear algebra, multivariate calculus, basic complex analysis, exterior forms, the Lebesgue integral, and differential geometry in R^n, and
  • ending with the integral theorem of Stokes and the theory of the topological degree of a mapping.

    In addition, automatically generated formulations of these statements in ordinary mathematical English will be provided.
    Most likely, the proof steps given explicitly in the lecture notes (and their English translations) will be available in the database, too. Whether we shall continue to refine the resulting informal (but formally stated) proof into fully formalized, automatically verified proofs will depend on the way the project develops and is funded.

    ALA words
    A list of over 4400 distinct German words occurring in the ALA lecture notes. This will become the core of the dictionary for formal mathematical German in the FMathL system.

    ALA sentences
    A list of approximately 4000 preprocessed sentences occurring in the ALA lecture notes. This will be the starting point for creating a grammar for formal mathematical German in the FMathL system.

    ALA grammar
    This is a report on work in progress for the FMathL project. It describes a preliminary grammar for parsing significant parts of the lecture notes for analysis and linear algebra by Arnold Neumaier.

    home pages of Peter Schodl and Kevin Kofler, who analyze ALA.


    Comments on some systems related to FMathL

    Systems related to the FMathL vision
    This document describes a number of systems available in 2010 related to the FMathL vision, and some of their limitations when viewed in the light of this vision.

    Limitations in Content MathML
    This technical report summarizes issues and limitations with Content MathML we encountered during our effort to represent example formulas which reflect common usage in mathematical texts. We conclude that Content MathML is currently not an adequate representation for our goals.

    Limitations in OpenMath
    This technical report summarizes the issues and limitations with OpenMath we encountered during our effort to represent commonly used mathematical formulas, leaving us to conclude that in its current state, OpenMath is not an adequate representation for our goals.


    A semantic virtual machine

    The implementation of FMathL will be based on the concept of a semantic mapping, a binary operation on a suitable set whose elements are called objecs. Given such a mapping, the objects may be viewed as the nodes of a natural labelled directed graph that stores all concepts of interest together with their properties and interrelations.

    A semantic virtual machine (SVM) is a variant of a programmable register machine that provides a clearly arranged assembler-style programming language and a user-friendly representation of semantic information in terms of the semantic memory, a time-dependent semantic mapping.

    This paper describes the concept of the SVM, its memory management and flow control, and shows how a semantic virtual machine can simulate any Turing machine. Analogous to a universal Turing machine, a universal semantic virtual machine (USVM) - a special SVM that can simulate every SVM - is given.


    MathResS - a mathematical research system

    MathResS: An automatic mathematical research system
    This is currently just the abstract of a project still in the proposal phase. Here are a more extensive version. Some related pages are:

    Mathematical reasoning, a bottom-up approach

    An automatic mathematical assistant - a vision

    What would you want from an automatic mathematical research assistant?
    Dozens of replies to some questions I had posed in various electronic communities

    Quotes on formalized mathematics and automatic mathematical assistants, collected from the Web

    What is mathematics?


    Slides

    MoSMath - A modeling system for mathematics by Peter Schodl
    Slides of a lecture at the Seminar Formale Mathematik of the Naproche project

    FMathL - Formal Mathematical Language by Arnold Neumaier
    Slides for a lecture at the AUTOMATHEŘ 2009 workshop

    FMathL, Mathematica, and Wolfram|Alpha by Arnold Neumaier
    How FMathL might alleviate conceptual limitations of Mathematica and Wolfram|Alpha

    FMathL Formal Mathematical Language by Peter Schodl
    Slides for a lecture at the conference on Mathematical Knowledge Management 2009

    FMathL Formal Mathematical Language - and how it relates to the Grammatical framework (GF) by Kevin Kofler
    Slides for a lecture at the GF Resource Grammar Summer School 2009

    Mathematik - Sprache und Werkzeug der Naturwissenschaften


    Computer-assisted proofs


    A. Neumaier, Computer-assisted proofs, in: (W. Luther and W. Otten, eds.) Proc. 12th GAMM-IMACS Symp. Sci. Comp., (SCAN 2006). IEEE Computer Society, 2007.
    ps.gz file (102K), pdf file (111K)
    This paper discusses the problem what makes a computer-assisted proof trustworthy, the quest for an algorithmic support system for computer-assisted proof, relations to global optimization, an analysis of some recent proofs, and some current challenges which appear to be amenable to a computer-assisted treatment.


    T. Rage, A. Neumaier and C. Schlier, Rigorous verification of chaos in a molecular model, Phys. Rev. E. 50 (1994), 2682-2688.
    download

    The Thiele-Wilson system, a simple model of a linear, triatomic molecule, has been studied extensively in the past. The system exhibits complex molecular dynamics including dissociation, periodic trajectories and bifurcations. In addition, it has for a long time been suspected to be chaotic, but this has never been proved with mathematical rigor.

    In this paper, we present numerical results that, using interval methods, rigorously verify the existence of transversal homoclinic points in a Poincare map of this system. By a theorem of Smale, the existence of transversal homoclinic points in a map rigorously proves its mixing property, i.e., the chaoticity of the system.


    Some other FMathL-related papers by our group


    Some links to related topics


    Common mathematical language (CML)

    Is mathematics a language? (a SIAM News article by Philip Davis)

    Mathematics as a language (from Wikipedia)

    Mathematics as a Language (from Cut The Knot)

    Handbook of Mathematical Discourse (by Charles Wells)

    A language for mathematical knowledge management (by Kieffer, Avigad and Friedman)

    Formal mathematics in natural language?

    Towards an Interactive Mathematical Proof Language (by Henk Barendregt)

    Computerising mathematical texts in MathLang

    A refinement of de Bruijn's formal language of mathematics (by Kamareddine and Nederpelt)

    Natural Language Processing of Mathematical Texts in mArachna (2007, by Blanke et al.)

    Translating Mathematical Vernacular into Knowledge Repositories (by Grabowski and Schwarzweiler)

    Computer-assisted reasoning with natural language: Implementing a mathematical vernacular (1998, by Callaghan and Luo)
    from the TYPES project (formerly at http://www.dur.ac.uk/TYPES/)

    DIALOG, natural mathematical language tutorial dialog with a student

    Math as a Language (by Dave Moursund)

    Math as a Natural Language (blog by Hal Daume)


    Translating proofs into natural language

    creating math text from proof assistant output

    How to write a nice, fully formalized proof (by Arnold Neumaier)

    W. Neumaier, Irrationality of the square root of 2. Proofs in a universal logic calculus, Manuscript, Juni 2022.
    This paper gives a detailed formal proof of a well-known result that translates fairly nicely into a human-readable proof.

    Social Processes and Proofs of Theorems and Programs (by De Millo, Lipton and Perlis)

    Understanding Informal Mathematical Discourse (by Claus Zinn)

    P.rex interactive natural language proof explanation system

    Nuprl Proof Translation Study

    Formal Proof Sketches (by Freek Wiedijk)

    The language of proofs

    Naproche natural language proof checking
    Linguistics and logic of common mathematical language

    Semantik-basierte Autorenwerkzeuge für mathematische Dokumente (by Autexier, Busemann and Wagner)

    And so on... Reasoning with infinite diagrams (by Solomon Feferman)

    Common sense for concurrency and inconsistency tolerance using Direct Logic(TM) (by Carl Hewitt)

    Proof style in the math subject wikis (on proofs in group theory and the facts they use)

    Suggested Upper Merged Ontology (SUMO) Gneral concept ontology


    LaTeX

    Translating latex into editor-ready form, HTML, XML, or Braille; interfaces with LaTeX output

    LaTeX

    LaTeX for logicians

    Idxtool, LaTeX "parser", very low level

    Eine einfache Grammatik für LaTeX, LaTeX "grammar" which detects low-level constructs, but no structure

    HeVeA, LaTeX to HTML translator, works by invoking LaTeX with some commands redefined

    LaTeX2HTML, complex LaTeX to HTML translator handwritten in Perl

    LyX, a WYSIWYM (What You See Is What You Mean) document processor using LaTeX and a LaTeX-style internal representation

    tex2lyx, LyX LaTeX parser, handwritten, context-dependent

    TeXmacs, another WYSIWYM (TeXmacs calls it WYSIWYW = What You See Is What You Want) document processor using LaTeX and a LaTeX-style internal representation
    Their internal representation (and thus also their LaTeX parser) does not accurately reflect structure though.

    Kile, LaTeX IDE with syntax highlighting
    Its syntax highlighting definition, basically a deterministic pushdown automaton, could be converted to a context-free grammar

    arXMLiv: Translating the arXiv to XML+MathML
    ... we try to translate the vast collection of scientific knowledge captured in the arXiv repository into content-based form [...] We have processed more than half of the arXiv collection (one run is a processor-year-size undertaking) and already have a success rate of over 50% (i.e. over 50% of the documents ran through without LaTeXML noticing an error).

    Hermes, grammar based translator from (AMS)LaTeX to Unicode(utf-8) encoded XML+MathML+metadata (from the MoWGLI project)
    Uses semantic LaTeX macros available in the Hermes distribution. Needs prior editing with semantic information.

    LaTeXML, LaTeX to XML converter written in Perl
    Handwritten parser using reimplementations of common LaTeX stylesheets, outputs XML that respects the structure of the document and can be easily reparsed

    Tralics, LaTeX to XML converter written in C++
    Handwritten parser using reimplementations of common LaTeX stylesheets, outputs XML that respects the structure of the document and can be easily reparsed

    Tools for Converting LaTeX to XML, list of LaTeX to XML converters
    with more options that may or may not be worth looking into

    CADiZ LaTeX interface for Z notation

    LaTeX2Tri: Physics and Mathematics for the Blind or Visually Impaired

    MathBraille; a system to transform LATEX documents into Braille

    LaTeX Bridge to Accessible Mathematical Presentation for blind people

    latex4blind: Latex For Blind Computer Users


    Digital mathematical libraries

    PlanetMath, free, collaborative online mathematical encyclopedia, written in LaTeX

    Formal Digital Library

    Digital Math by Alphabet

    NSDL, National Science Digital Library for education and research in Science, Technology, Engineering, Mathematics

    HELM - Hypertextual Electronic Library of Mathematics

    MathWeb, supporting mathematics on the web

    Connexions, an environment for collaboratively developing, freely sharing, and rapidly publishing scholarly content on the Web.


    Mathematics on the web

    OpenMath for representing the semantics of mathematical objects

    MathML, a low-level specification for describing mathematics as a basis for machine to machine communication

    Phrasebooks, OpenMath interfaces to various computer algebra systems (GAP, Mathematica, Magma)

    OMDoc markup format for Open Mathematical Documents.

    MathWeb infrastructure for web-supported mathematics, using OMDoc

    MBase: A Mathematical Knowledge Base, as part of MathWeb

    Math Web Search, A Search Engine for Mathematical Formulae

    Wolfram|Alpha, search engine allowing (limited) mathematical queries

    WebALT: Web Advanced Learning Technologies

    vdash, wiki of formalized math

    MathWiki -- a Web-based Collaborative Authoring Environment for Formal Proofs

    SWiM, semantic wiki for collaboratively building, editing and browsing a mathematical knowledge base

    Maths for More, advanced calculation and presentation tools for mathematics education

    Joining Educational Mathematics, thematic network for the coordination of content enrichment activities in the area of mathematics for e-learning platforms


    The semantic web

    RDF, Resource Description Framework

    RDF Semantics

    OWL, Web Ontology Language

    The Semantic Desktop

    Nepomuk-KDE (KDE version of the Semantic Desktop)

    Tracker (Gnome version of the Semantic Desktop)


    Problem collections

    TPTP, The TPTP Problem Library for Automated Theorem Proving

    TSTP, The TSTP Solution Library for Automated Theorem Proving

    Theorem Proving Competition

    QBFLIB, Quantified Boolean Formulas Satisfiability Library

    SATLIB - The Satisfiability Library (last maintained 2003)

    CSPLIB: a problem library for constraints

    The ILTP Library, Benchmarking Theorem Provers for Intuitionistic Logic

    OR-Library, combinatorial optimization and structured constraint satisfaction problems

    QPQ Deductive Software Repository, a forum for developing and exchanging formal content including theorem proving and verification systems, libraries, benchmarks, challenges, standards, and technical reports


    Constraint satisfaction

    Tools and competitions for solving SAT (Boolean satisfaction) problems

    SAT Live!

    SAT Competitions

    SAT 2005 Competition

    MiniSat, a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.


    Proof assistants

    The Coq proof assistant

    Pcoq, graphical user interface for COQ

    Vampire resolution theorem prover

    Metamath Proof Explorer Home Page

    Mizar (the language of the journal ''Formalized mathematics'')

    Theorema

    PVS Specification and Verification System

    ProofPower, tools supporting specification and formal proof in Higher Order Logic (HOL) and in the Z notation

    The PhoX Proof Assistant

    PRL and Nuprl for formal computational mathematics

    OMEGA, Agent-oriented Proof Planning

    MINLOG, interactive formal proof system

    ACL2, a development of Nqthm, the Boyer-Moore prover

    The LEGO Proof Assistant

    Agda proof assistant

    SAD, System for Automated Deduction

    CALCULEMUS, network of research groups and individuals interested in the integration of the deduction and the computational power of automated deduction systems and computer algebra systems

    SAD/ForTheL, System for Automated Deduction
    intended for automated processing of formal mathematical texts written in a special language called ForTheL (FORmal THEory Language) or in a traditional first-order language.


    Theorem provers

    Lean theorem prover

    Isar - Intelligible semi-automated reasoning, for the Isabelle theorem prover
    IsarMathLib, library of formalized mathematics for the Isabelle/Isar proof assistant

    The HOL Light theorem prover

    Prover9 and Mace4 (successor of the Otter prover)

    Otter-lambda, theorem-proving program

    SPASS: An Automated Theorem Prover for First-Order Logic with Equality

    The E Equational Theorem Prover

    E-SETHEO, compositional theorem prover for first-order logic with equality

    Matita, simple COQ-like theorem prover

    IMPS, An Interactive Mathematical Proof System

    Equinox, automated theorem prover for pure first-order logic with equality

    Paradox, finite-domain model finder for pure first-order logic with equality, via a sequence of SAT problems

    KeYmaera: A Hybrid Theorem Prover for Hybrid Systems

    The CADE ATP System Competition
    The World Championship for 1st Order Automated Theorem Proving

    User-Interfaces for Theorem Provers (Proceedings of UITP'06)

    The Seventeen Provers of the World (by Freek Wiedijk)

    Formalizing 100 theorems (by Freek Wiedijk)


    Logical frameworks

    Alfa proof editor

    The Twelf Project


    Term rewrite systems

    Waldmeister, theorem prover for unit equational logic using unfailing Knuth-Bendix completion

    AProVE, Automated Program Verification Environment, a system for automated termination and innermost termination proofs of term rewrite systems

    Slothrop, automated equational theorem prover that performs a variant of Knuth-Bendix completion

    CiME, rewriting toolbox that provides Coq certificates for termination proofs (standard rewriting)


    Specification

    The Z Notation: a reference manual
    ISO Standard for Z notation
    Z notation examples

    PVS Specification and Verification System

    Abstract State Machines

    Semantics

    HATS, Highly Adaptable and Trustworthy Software using Formal Methods
    The technical core of the project is an Abstract Behavioural Specification (ABS) language


    Solvers

    Applications of Quantified Constraint Solving over the Reals (mathematically rigorous, by Stefan Ratschan)

    QEPCAD, Quantifier Elimination by Partial Cylindrical Algebraic Decomposition (mathematically rigorous)

    REDLOG REDuce LOGic system

    ModSim

    Exact Computation

    Eqlog: An Equational Logic Programming Language

    QPQ Deductive Software Repository

    Hilbert II - QED continuation

    MoWGLI Home Page

    Logosphere

    TYPES topical workshop: Math Wiki


    Mathematical assistants

    Maple

    Mathematica

    MuPAD

    Macsyma, MAXIMA, Vaxima

    Mathematical Assistant on the Web (interface to Maxima)

    Derive: The Mathematical Assistant

    Omega: Towards a Mathematical Assistant (1997)

    Proof development with Omega (2002)

    Mathematical Assistants

    Theorema: A Mathematical Assistant System based on Mathematica

    Ozlo Mathematical Assistant (very simple only)

    Convergence on Mathematics Assistants (ConvMathAssist)

    DIALOG: Natural Language-based Interaction with a Mathematics Assistance System

    A Grand Challenge for Computing Research: a mathematical assistant (by Toby Walsh)

    Computer-supported formal work: Towards a digital mathematical assistent (2007, Mizar based)

    Project Proposal: Mathematical Assistant (simple)

    Math Assistant, designed to help you with routine math tasks (simple)

    Digital Math by Alphabet
    This is an overview of systems implementing "mathematics in the computer" as compiled by Freek Wiedijk

    Automatic Learning in Proof Planning (2003)

    Integration of Interactive and Automatic Provers (Vampire)

    Automatic Concept Formation in Pure Mathematics (1999, by Colton, Bundy and Walsh)

    On the Notion of Interestingness in Automated Mathematical Discovery (2000, by Colton, Bundy and Walsh)

    Mathematical Assistants


    Computer algebra systems

    GAP - Groups, Algorithms, Programming - a System for Computational Discrete Algebra

    LTP, Lie Tools Package (Lie algebra computations in Maple)

    LiE, computer algebra package for Lie group computations

    VFLIB graph matching for isomorphism and graph-subgraph isomorphism

    NAUTY -- Graph Isomorphism in C
    nauty summary

    Epsilon Software Tool for Polynomial Elimination and Decomposition

    Orbital library, comprises theorem proving, computer algebra, search and planning, as well as machine learning algorithms.

    Computer Algebra Information Network

    The Stony Brook Algorithm Repository for combinatorial algorithms


    Modeling languages

    AMPL

    GAMS


    Problem solving environments

    How to use mathematical concepts and statements from Tricki,store of useful mathematical problem-solving techniques

    ProofWiki, online compendium of mathematical proofs

    Problem Solving Environments (1998)

    Projects, Products, Applications and Tools (1998)


    Formalized mathematics

    Formalized Mathematics (AutoMath), Nuprl Library

    Formalized Mathematics
    How to build a library of formalized mathematics

    Research/Formalizing Mathematics - Foundations

    Formalizing Mathematics

    What is Formalized Mathematics (by W.M. Farmer)

    The formalization of mathematics (by Harvey Friedman)

    Formalized Mathematics (by John Harrison, 1996)

    The challenge of computer mathematics(2005, by Barendregt and Wiedijk)

    Towards Practical Reflection for Formal Mathematics (by Giese and Buchberger)

    Closing the Gap Between Formal and Digital Libraries of Mathematics (by Gow and Cairns) - Mizar orieneted

    Formal Mathematics in MathML

    Mathematics, Reasoning, and Software (2006)


    Formal proofs

    Formal Proof - Theory and Practice (by John Harrison, 2008)
    A paper from the December 2008 Special Issue on Formal Proof of the Notices of the American Mathematical Society

    Formal proof of the four color theorem in Coq

    How To (really) Trust A Mathematical Proof (from Science News)

    MathScheme, An Integrated Framework For Computer Algebra And Computer Theorem Proving

    Computer Assisted Theorem Proving in Set Theory

    Mechanized Reasoning (not updated since 1999)

    The verifying compiler: A grand challenge for computing research (2003, by Tony Hoare)

    Ten Commandments of Formal Methods ... Ten Years Later (2007, by Bowen and Hinchey)

    Learning with LearnOmatic

    Rough structure and classification (by Timothy Gowers)
    With remarks on what constities a good proof

    Formal Proof Sketches (2004, by Freek Wiedijk)

    Verifying nonlinear real formulas via sums of squares (2007, by John Harrison)


    Semantics and language

    Grammatical framework (by Aarne Ranta)

    Expressivity and Complexity of the Grammatical Framework (by Peter Ljunglöf)

    Formal Mathematics in Informal Language (slides by Aarne Ranta)

    State of the art in multilingual and multicultural creation of digital mathematical content

    Attempto Controlled English (ACE), a controlled natural language, i.e. a rich subset of standard English designed to serve as specification and knowledge representation language.

    Greenstone, multilingual software for building and distributing digital library collections

    MultiNet, Knowledge Representation with Multilayered Extended Semantic Networks

    FDL, Formal digital library

    Computational Semantics Information

    Loglan artificial human language

    Euclid, Elements (ed. J. L. Heiberg)

    Euclid's Elements in Greek (by Richard Fitzpatrick)

    Ascii Table - ASCII character codes and html, octal, hex and decimal charts

    Loglan, a logical language
    ``There is a linguistic theory--known as the Sapir-Whorf hypothesis - that the structure of a human language sets limits on the thinking of those who speak it; hence a language could even place constraints on the development of the cultures that use it. If this hypothesis is correct, then a language that could lift those constraints, by reducing them to a minimum, ought thereby to release its speakers' minds from their ancient linguistic bonds, and that should have a profound effect, both on individual thinking and on the development of human cultures.''
    ``Loglan is a language designed to test this hypothesis. It was originally developed in the 1950s, and an early version was described in the Scientific American for June 1960. Since then, Loglan (a logical language) has continued to develop and expand. One aim in its development was to make the grammar free from ambiguity, and that aim has been achieved. Another aim was audio-visual isomorphism (which means that the Loglan speechstream breaks up automatically into fully punctuated strings of words), and this has been partially achieved. There are in any case no ambiguities in Loglan such as "ice cream" vs. "I scream": Loglan word boundaries are always clear. Moreover, much of Loglan grammar is based on the Predicate Calculus of modern mathematical logic...don't worry, you don't have to be a mathematician to learn Loglan, but you will probably enjoy the clarity of thought that its grammar encourages.''


    Choosing software

    Decision Tree for Optimization Software

    MONET, framework for the description and provision of web-based mathematical services


    Algorithms

    Literate Programming

    On the simplest and smallest universal Turing machine | Anima Ex Machina

    TM23Proof.pdf (application/pdf Object) (small Turing machine)

    Universal Turing Machine -- from Wolfram MathWorld

    Dictionary of Algorithms and Data Structures


    Projects

    The QED Manifesto

    Verifix, Provably Correct Compilers

    Zentity (codename Famulus), Research Output Repository Platform for creating and maintaining an organization's repository ecosystem
    and an associated weblog

    Evidence Algorithm (System for Automated Deduction - SAD)

    Theorema Project

    Cognitive Systems

    Mathematical Wiki

    Universal Logic

    Cognitive Science of Mathematics

    High School Mathematics (by Freek Wiedijk)


    Places

    RISC: Research Institute for Symbolic Computation

    AG Theoretische Informatik und Logik/Theory and Logic Group (research)

    Computational logic TU Wien


    Some People

    Jesse Alama

    Jeremy Avigad

    John Bell

    P. Cairns

    Razvan Diaconescu

    Solomon Feferman

    Dov Gabbay

    Dov Gabbay

    Herman Geuvers

    Georges Gonthier (MathComponents)

    Carl Hewitt

    Jaakko Hintikka

    Jaakko Hintikka

    Fairouz Kamareddine (MathLang)

    Saul Kripke

    John McCarthy

    Andrei Paskevich

    Michael Kohlhase (OMDoc, ArXMLiv)

    Stefan Ratschan -- (P)reprints

    John Robinson

    Dana Scott

    Stephen Simpson (Foundations of Mathematics)

    Peter Smith (Logic Matters)

    Steve Stevenson

    Toby Walsh

    Freek Wiedijk

    Wolfgang Windsteiger

    Wolfgang Windsteiger

    Doron Zeilberger

    Doron Zeilberger

    Claus Zinn (formal analysis of natural language proofs) and his papers (in particular his thesis ''Understanding Informal Mathematical Discourse'')

    Some Philosophers


    Theoretical logic

    Mathematical Logic around the world

    Foundations of Mathematics resource list

    John Halleck's Logic Systems Axiom List

    Supertask - Wikipedia, the free encyclopedia

    Kurt Gödel Research Center for Mathematical Logic

    New Foundations Home Page

    Elementary Set Theory with a Universal Set (pdf of a book, by Randall Holmes)

    What is Foundations of Mathematics?

    Common sense for concurrency and inconsistency tolerance using Direct Logic(TM) (by Carl Hewitt)


    Conferences

    The MKM Interest Group (Mathematical Knowledge Management)

    Calculemus 2008

    MKM 2001 Proceedings


    Journals and papers

    Computer and Information Science Papers CiteSeer Publications ResearchIndex

    Logic Journals

    Journal of Formalized Mathematics (Mizar articles)


    Teaching

    Computer Assisted Proof in Mathematics Education


    Discussion

    FOM -- Foundations of Mathematics mailing list

    Foundation of Math mailing list Archives

    Augustine on infinity

    What is deep mathematics? (from Gower's Weblog)


    Supertasks

    A hierarchy of idealized computer architectures

    Infinite time Turing machines (by Hamkins and Lewis)

    Supertask (from Wikipedia)

    Mathematik, Physik und Ewigkeit (mit einem Augenzwinkern betrachtet)
    Ein Science-Fiction Interview


    Controversial

    The Law of Accelerating Returns (by Ray Kurzweil)

    The Church-Turing Thesis, Copeland's article commented

    1001 Reasons for Not Proving Your Programs Correct: a survey (by Steve Stevenson)


    Unclassified

    Compilers and compiler generators

    Hypertree Decompositions



    Some of My Other Pages


    Global Optimization
    Interval Methods
    Mathematical Software
    Computational Mathematics Links
    Mathematics Links
    Statistics Links
    Artificial Intelligence
    A Theoretical Physics FAQ

    my home page (http://arnold-neumaier.at/)

    Arnold Neumaier (Arnold.Neumaier@univie.ac.at)