Let's write an automated theorem prover! A series of increasingly sophisticated automated theorem provers realized as Prolog-like language implementations using Warren's Abstract Machine.

Ruby とオブジェクト指向による四色定理

Thousands of Problems for Theorem Provers Library

Automatic Proving System using Predicate Logic

A function to sum your sets of integers in a flash !

四色定理を Haskell に移植したよ

四色定理を F# に移植したよ

This application is used for interactive proving of logical formulas. It supports propositional, intuitionist and predicate logic. It proves using natural deduction or sequent calculus. The proof is displayed as Gentzen or Fitch notation.