Oliver Help

Directions for Oliver

Oliver is an online system for logic proofs.At each step, you are presented with a partial proof.You must provide the next step in the proof.Your work will be checked to see that it is a logical conclusion of the steps so far. If it is, Oliver will accept the step. Otherwise you'll have to come up with a different step. When you have deduced the conclusion, the proof is complete and Oliver will stop.

Since logic proofs require symbols not on an ordinary keyboard, you must type in formulae using similar looking symbols. The normal symbols you need for logic proofs are

^ conjunction 
v inclusive disjunction 
-> implication 
<-> equivalence 
~ negation 
( left parenthesis 
) right parenthesis

Operators have the same precedence they normally would. Namely

Expressions in Parenthesis have highest precedence
Negation has second highest precedence
Conjunction has the next highest precedence
Disjunction has the next highest precedence
Implication and Equivalence have the lowest precedence

Example Proof
This is what a finished proof looks like

line statement justification

1 pqr premise

2 sq premise

3 t premise

4 pt premise

5 prs premise

6 p 3,4

7 r 1,6

8 pr 6,7

9 s 5,8

10 q 9,2

line	statement	justification
1	pqr	premise
2	sq	premise
3	t	premise
4	pt	premise
5	prs	premise
6	p	3,4
7	r	1,6
8	pr	6,7
9	s	5,8
10	q	9,2

Directions for Oliver

Example Proof