| ||||||||
|---|---|---|---|---|---|---|---|---|
| ||||||||
The System for Automated Deduction is being developed in the frame of the 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 SAD system is a free open-source software issued under the GNU GPL. You can download it either as a source package or as a source package with precompiled binaries (Linux i386) from the Download page. 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:
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 native 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 Saarbrücken, Germany.
In the distributed package, SAD is configured to work also with
Vampire,
E prover,
Prover9,
and Otter.
One can easily employ any prover taking input problems
in a standard format such as TPTP or DFG. | ||||||||
|
