 

 
The System for Automated Deduction accepts onegoal firstorder sequents in the form of a sequence of dotterminated 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 wellformed formulas. We adopt the following notation (in parentheses, alternative names are shown):
Enter a firstorder 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.
Examples:
 
