The System for Automated Deduction is being developed in the frame of EA project. The system is 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. To know more about the input languages of SAD, you can see the Explanations page, the examples of sequents, theorems, texts, and the Reference Manual on ForTheL (gzipped PS or PDF).

The system SAD is a free open-source software issued under the GNU GPL. You can download the current release of SAD either as a source package or as a source package with precompiled binaries (Linux x86, glibc 2.3). The older releases are also available.

The hyperlinks below provide an online access to the current version of SAD. Fill the form with a ForTheL text or a first-order sequent to process, set the parameters of proof search, and launch a command. SAD will process your task and return the resulting translation, proof, or verification trace. In its current implementation, SAD executes the following four tasks:

• Inference Search:  establish deducibility of a first-order sequent;
• Theorem Proving:  prove a proposition in the context of a ForTheL-text;
• Text Verification:  verify a self-contained ForTheL-text;
• TPTP Problems:  download and prove a problem from the TPTP Library.

Every line in the resulting output is "signed" by some module of SAD. The modules [ForTheL] and [FOL] are the parsers of ForTheL and the first-order language, respectively. The module [TPTP] parses TPTP problems and axiom sets. The module [Reason] manages the main cycle of SAD and formulates tasks for [Moses], the prover of SAD.

As an alternative background prover, you can use SPASS, a powerful resolution-based prover for first-order logic with equality. SPASS is developed in Max Plank Institute for Informatics in Saarbruecken, Germany.