Demonstrates how to use Coq in Emacs for machine-assisted theorem proving.

Tools for formal reasoning, written in Haskell.

References on the relation between programs, proofs, and (undelimited and delimited) continuations.

Mathematics developed in complete detail from first principles, with absolute rigor (computer verified proofs).

A formal sketch of how category theory can serve to clarify the analogies between physics, topology, logic and computation.

A program in mathematical logic that seeks to determine which axioms are required to prove certain theorems of mathematics.

The analysis of formalized proofs to obtain explicit bounds and convergence rates from proofs that, when expressed in natural language, appear to be nonconstructive.

A game of inductive logic in which the Master creates a rule and the Students attempt to discover it by building and studying arrangements of plastic pyramid-shaped pieces.

Class covering different systems of logic, set theory, basic meta-math and recursive function theory.

PTTP is an implementation of the model elimination theorem-proving procedure that extends Prolog to the full first-order predicate calculus.

Lambda Prolog is a logic programming language featuring polymorphic typing, modular programming, and higher-order programming. It can capture higher-order abstract syntax and thus map object-level bindings to programming language bindings.

Darwin is an automated theorem prover for first order clausal logic and the first implementation of the Model Evolution Calculus.

The Mizar project started around 1973 as an attempt to reconstruct mathematical language in a computer-oriented environment. The most important activity has been the development of a database for mathematics.

One of the justifications for the use of Bayesian probability theory. Probability is interpreted as a formal system of logic, the natural extension of Aristotelian logic into the realm of reasoning in the presence of uncertainty.

Implies that every arbitrarily long proof for any statement in propositional logic can be formalized (in polynomial time), so that one can check whether it is correct or not by only reading a constant number of letters from it!

A crash course in the mathematics behind Turing's results and how it applies to the very practical problem of programming in C. Explains the connection between Turing Machines, Lambda Calculus, types, Classical Logic and proofs.

Possibilities of modeling pathological expressions in formal and natural languages. May in part be relevant for models where classical decision theory breaks down due to infinite recursion.

Daemon Proof Checker, Quizmaster, Countermodel Checker, Wff Checker, Equivalency Checker.

How it came to be recognized that proofs and programs are the same thing is a story that spans a century. At the end of the story is a new principle for designing programming languages that will guide computers into the 21st century.

If a theorem contains more information than a given set of axioms, then it is impossible for the theorem to be derived from the axioms. This suggests that the incompleteness phenomenon discovered by Gödel is natural and widespread [..].

For any consistent formal theory that proves basic arithmetical truths, it is possible to construct an arithmetical statement that is true but not provable in the theory. That is, any consistent theory of a certain expressive strength is incomplete.

In a theory with Peano arithmetic, for any formula P, if it is provable that "if P is provable then P", then P is provable.