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):

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]