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://www.mat.univie.ac.at/~neum/FMathL.html and contains sections on
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
The goal of the FMathL project is to combine
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.
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.
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.
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
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:
Towards a Computer-Aided System for Real Mathematics (an extended thread in the n-Category Cafe, related to FMathL and categorial foundations of mathematics)
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.
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
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.
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).
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,
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.
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.
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.
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
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
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
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)
creating math text from proof assistant output
Social Processes and Proofs of Theorems and Programs (by De Millo, Lipton and Perlis)
Understanding Informal Mathematical Discourse (by Claus Zinn)
How to write a nice, fully formalized proof (by Arnold Neumaier)
P.rex interactive natural language proof explanation system
Formal Proof Sketches (by Freek Wiedijk)
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
Translating latex into editor-ready form, HTML, XML, or Braille; interfaces with LaTeX output
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
PlanetMath, free, collaborative online mathematical encyclopedia, written in LaTeX
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.
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
RDF, Resource Description Framework
Nepomuk-KDE (KDE version of the Semantic Desktop)
Tracker (Gnome version of the Semantic Desktop)
TPTP, The TPTP Problem Library for Automated Theorem Proving
TSTP, The TSTP Solution Library for Automated Theorem Proving
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
Tools and competitions for solving SAT (Boolean satisfaction) problems
MiniSat, a minimalistic, open-source SAT solver, developed to help researchers and developers alike to get started on SAT.
Pcoq, graphical user interface for COQ
Vampire resolution theorem prover
Metamath Proof Explorer Home Page
Mizar (the language of the journal ''Formalized mathematics'')
PVS Specification and Verification System
ProofPower, tools supporting specification and formal proof in Higher Order Logic (HOL) and in the Z notation
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
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.
Isar - Intelligible semi-automated reasoning,
for the Isabelle theorem prover
IsarMathLib, library of formalized mathematics for the
Isabelle/Isar proof assistant
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)
Alfa proof editor
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)
The Z Notation: a reference manual
ISO Standard for Z notation
Z notation examples
PVS Specification and Verification System
HATS, Highly Adaptable and Trustworthy Software using Formal Methods
The technical core of the project is an Abstract Behavioural
Specification (ABS) language
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
Eqlog: An Equational Logic Programming Language
QPQ Deductive Software Repository
TYPES topical workshop: Math Wiki
Mathematical Assistant on the Web (interface to Maxima)
Derive: The Mathematical Assistant
Omega: Towards a Mathematical Assistant (1997)
Proof development with Omega (2002)
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)
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
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 (AutoMath), Nuprl Library
Formalized Mathematics
How to build a library of formalized mathematics
Research/Formalizing Mathematics - Foundations
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
Mathematics, Reasoning, and Software (2006)
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)
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)
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
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.''
Decision Tree for Optimization Software
MONET, framework for the description and provision of web-based mathematical services
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
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)
Cognitive Science of Mathematics
High School Mathematics (by Freek Wiedijk)
RISC: Research Institute for Symbolic Computation
AG Theoretische Informatik und Logik/Theory and Logic Group (research)
Georges Gonthier (MathComponents)
Fairouz Kamareddine (MathLang)
Michael Kohlhase (OMDoc, ArXMLiv)
Stefan Ratschan -- (P)reprints
Stephen Simpson (Foundations of Mathematics)
Peter Smith (Logic Matters)
Claus Zinn (formal analysis of natural language proofs) and his papers (in particular his thesis ''Understanding Informal Mathematical Discourse'')
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
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)
The MKM Interest Group (Mathematical Knowledge Management)
Computer and Information Science Papers CiteSeer Publications ResearchIndex
Journal of Formalized Mathematics (Mizar articles)
Computer Assisted Proof in Mathematics Education
FOM -- Foundations of Mathematics mailing list
Foundation of Math mailing list Archives
What is deep mathematics? (from Gower's Weblog)
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
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)
Compilers and compiler generators
my home page (http://www.mat.univie.ac.at/~neum/)
Arnold Neumaier (Arnold.Neumaier@univie.ac.at)