Journal of Formalized Reasoning

Last updated

Abstracting and indexing

The journal is abstracted and indexed in Scopus, MathSciNet, and Zentralblatt MATH .


Related Research Articles

<span class="mw-page-title-main">Gregory Chaitin</span> Argentine-American mathematician

Gregory John Chaitin is an Argentine-American mathematician and computer scientist. Beginning in the late 1960s, Chaitin made contributions to algorithmic information theory and metamathematics, in particular a computer-theoretic result equivalent to Gödel's incompleteness theorem. He is considered to be one of the founders of what is today known as algorithmic complexity together with Andrei Kolmogorov and Ray Solomonoff. Along with the works of e.g. Solomonoff, Kolmogorov, Martin-Löf, and Leonid Levin, algorithmic information theory became a foundational part of theoretical computer science, information theory, and mathematical logic. It is a common subject in several computer science curricula. Besides computer scientists, Chaitin's work draws attention of many philosophers and mathematicians to fundamental problems in mathematical creativity and digital philosophy.

<span class="mw-page-title-main">Alfred Tarski</span> American mathematician

Alfred Tarski was a Polish-American logician and mathematician. A prolific author best known for his work on model theory, metamathematics, and algebraic logic, he also contributed to abstract algebra, topology, geometry, measure theory, mathematical logic, set theory, and analytic philosophy.

<span class="mw-page-title-main">Karl Weierstrass</span> German mathematician (1815–1897)

Karl Theodor Wilhelm Weierstrass was a German mathematician often cited as the "father of modern analysis". Despite leaving university without a degree, he studied mathematics and trained as a school teacher, eventually teaching mathematics, physics, botany and gymnastics. He later received an honorary doctorate and became professor of mathematics in Berlin.

<span class="mw-page-title-main">American Mathematical Society</span> Association of professional mathematicians

The American Mathematical Society (AMS) is an association of professional mathematicians dedicated to the interests of mathematical research and scholarship, and serves the national and international community through its publications, meetings, advocacy and other programs.

<span class="mw-page-title-main">Mizar system</span>

The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec.

The QED manifesto was a proposal for a computer-based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically.

<span class="mw-page-title-main">Mathematics education</span> Mathematics teaching, learning and scholarly research

In contemporary education, mathematics education—known in Europe as the didactics or pedagogy of mathematics—is the practice of teaching, learning, and carrying out scholarly research into the transfer of mathematical knowledge.

MathWorld is an online mathematics reference work, created and largely written by Eric W. Weisstein. It is sponsored by and licensed to Wolfram Research, Inc. and was partially funded by the National Science Foundation's National Science Digital Library grant to the University of Illinois at Urbana–Champaign.

Lists of mathematics topics cover a variety of topics related to mathematics. Some of these lists link to hundreds of articles; some link only to a few. The template to the right includes links to alphabetical lists of all mathematical articles. This article brings together the same content organized in a manner better suited for browsing. Lists cover aspects of basic and advanced mathematics, methodology, mathematical statements, integrals, general concepts, mathematical objects, and reference tables. They also cover equations named after people, societies, mathematicians, journals, and meta-lists.

<span class="mw-page-title-main">MathWorks</span> Company that produces mathematical computing software

MathWorks is an American privately held corporation that specializes in mathematical computing software. Its major products include MATLAB and Simulink, which support data analysis and simulation.

In mathematics, Hilbert's program, formulated by German mathematician David Hilbert in the early 1920s, was a proposed solution to the foundational crisis of mathematics, when early attempts to clarify the foundations of mathematics were found to suffer from paradoxes and inconsistencies. As a solution, Hilbert proposed to ground all existing theories to a finite, complete set of axioms, and provide a proof that these axioms were consistent. Hilbert proposed that the consistency of more complicated systems, such as real analysis, could be proven in terms of simpler systems. Ultimately, the consistency of all of mathematics could be reduced to basic arithmetic.

Mathematical Reviews is a journal published by the American Mathematical Society (AMS) that contains brief synopses, and in some cases evaluations, of many articles in mathematics, statistics, and theoretical computer science. The AMS also publishes an associated online bibliographic database called MathSciNet which contains an electronic version of Mathematical Reviews and additionally contains citation information for over 3.5 million items as of 2018.

zbMATHOpen, formerly Zentralblatt MATH, is a major reviewing service providing reviews and abstracts for articles in pure and applied mathematics, produced by the Berlin office of FIZ Karlsruhe – Leibniz Institute for Information Infrastructure GmbH. Editors are the European Mathematical Society, FIZ Karlsruhe, and the Heidelberg Academy of Sciences. zbMATH is distributed by Springer Science+Business Media. It uses the Mathematics Subject Classification codes for organising reviews by topic.

Robert Duncan Luce was an American mathematician and social scientist, and one of the most preeminent figures in the field of mathematical psychology. At the end of his life, he held the position of Distinguished Research Professor of Cognitive Science at the University of California, Irvine.

In physics and cosmology, the mathematical universe hypothesis (MUH), also known as the ultimate ensemble theory, is a speculative "theory of everything" (TOE) proposed by cosmologist Max Tegmark.

MathSciNet is a searchable online bibliographic database created by the American Mathematical Society in 1996. It contains all of the contents of the journal Mathematical Reviews (MR) since 1940 along with an extensive author database, links to other MR entries, citations, full journal entries, and links to original articles. It contains almost 3.6 million items and over 2.3 million links to original articles.

<span class="mw-page-title-main">Mathematical sociology</span> Interdisciplinary field of research

Mathematical sociology or the sociology of mathematics is an interdisciplinary field of research concerned both with the use of mathematics within sociological research as well as research into the relationships that exist between maths and society.

<span class="mw-page-title-main">Andrzej Trybulec</span> Polish mathematician and computer scientist

Andrzej Wojciech Trybulec was a Polish mathematician and computer scientist noted for work on the Mizar system.

Mathematics is a field of study that investigates topics such as number, space, structure, and change.

Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types. Types in univalent foundations do not correspond exactly to anything in set-theoretic foundations, but they may be thought of as spaces, with equal types corresponding to homotopy equivalent spaces and with equal elements of a type corresponding to points of a space connected by a path. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by "categorical" mathematics in the style of Alexander Grothendieck. Univalent foundations depart from the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory. The development of univalent foundations is closely related to the development of homotopy type theory.