SAD system Explanations Download Our Team
Inference Search Theorem Proving Text Verification TPTP Problems

The System for Automated Deduction accepts one-goal first-order sequents in the form of a sequence of dot-terminated formulas where the goal formula is separated from premises by a colon. Thus, a sequent  P1, P2, P3 -> G  is written as  P1. P2. P3. : G.  Sequents with the empty goal are also allowed, in the form  P1. P2. P3. :  

Formulas are built from tokens: variables, function symbols and predicate symbols, with the help of the propositional connectives, quantifiers and parentheses. You can also use Church's dot to group subformulas. Note that we use the same character to terminate formulas as this is unambiguous for well-formed formulas. We adopt the following notation (in parentheses, alternative names are shown):

 @  (forall  universality    $  (exists  existence  
 ~  (iff  equivalence    >  (implies  implication  
 |  (or  disjunction    &  (and  conjunction  
 -  (not  negation    .    Church's dot  
 =    equality    !=    disequality  
 true    verum    false    falsum  

Enter a first-order sequent in the window below. Use the command [Prove with Moses] to launch the prover of SAD, Moses, or the command [Prove with] to use an external prover.


  1. A simple lemma of the group theory. [Try this example]

to Russian Last modified: 11 Oct 2007