Talos Online

Automated Theorem Proving by RAIR Labs

DCEC Logical Proof Generator

  • Enter your API Key; if you do not have an API Key, contact RAIR labs to receive one.
  • Enter any prototypes that are needed for your proof. The standard set of DCEC functions and sorts are pre-prototyped.
  • Enter a series of DCEC statements into the Axioms field, in either S or F notation. One statement per line, please.
  • Enter a DCEC statement as a conjecture, also in either S or F notation.
  • If you would like the prover to justify any proofs with the Axioms used, select that option.
  • Enter a maximum time in the Timeout; if no time is selected the maximum time associated with your API Key will be used instead.
  • Enter any SPASS options you wish to add to the prover in the Options field.
  • If you would like Simultaneous Reasoning, where all DCEC inference rules are only used when times are the same, check the box.
  • If you would like to receive any new DCEC statements the Prover proves, check the Discover box.
  • If you would like to allow or disallow certain rules, click the various 'Show Rules' buttons and check them appropriately.
  • Hit submit!














DCEC Rule 1
DCEC Rule 2
DCEC Rule 3
DCEC Rule 4
DCEC Rule 5
DCEC Rule 6
DCEC Rule 7
DCEC Rule 9
DCEC Rule 10
DCEC Rule 11a
DCEC Rule 11b
DCEC Rule 12
DCEC Rule 13
DCEC Rule 14
DCEC Rule 15

Modus Ponens
Conjunction Introduction
Simplification
Weakening
DeMorgan
Distribution
Commutativity of and
Commutativity of or
Commutativity of xor
Definition of xor
Disjunctive Syllogism
Cut-Elimination
Disjunction Elimination
Definition of iff

Modus Ponens
Conjunction Introduction
Simplification
Weakening
DeMorgan
Distribution
Commutativity of and
Commutativity of or
Commutativity of xor
Definition of xor
Disjunctive Syllogism
Cut-Elimination
Disjunction Elimination
Definition of iff

Super Erogatory Reasoning