OTTER Quick Start Tutorial

Getting started

1. Obtaining OTTER
   • If you have an RCS account.
   • All others.
2. Always run from the UNIX command prompt:
   otter < [INPUT FILE] > [OUTPUT FILE]
3. Input File skeleton:

       % Comment
       set(auto).
   
       formula_list(usable).
   
         % All well-formed formulas go here
   
       end_of_list.
   

4. Be sure to end each line with a period

Syntax

FIRST ORDER LOGIC	<======>	OTTER
	AND	&
	OR	|
	NOT	-
	Conditional	->
	Biconditional	<->
	Existential Quantifier	exists
	Universal Quantififer	all

What OTTER outputs

• Making OTTER do a Proof By Contradiction
  If you include a contradictory statement in your formula_list OTTER will attempt a proof:
  • Socrates is mortal example.
  • Family example.
• Making OTTER Chug
  Force OTTER to come to a conclusion by excluding the contradictory statement in your formula_list:
  • Socrates is mortal example.
  • Family example.