george: User Manual

[ Introduction ] [ File Structure ] [ #check PROP ] [ #check PRED ] [ #check TP ]
[ #check ND ] [ #check ST ] [ Arithmetic ] [ Sets ] [ #check Z ] [ #check PC ]
[ Contributions by Students ] [ Credits ] Keywords ]

Transformational Proofs (#check TP)

Here is an example of the response to a question that requires a transformational proof for propositional logic:

#check TP

! (r => ! ((p | r) & (r | q))) <->  r

1) ! (r => ! ((p | r) & (r | q)))
2) ! (r => ! ((r | p) & (r | q))) by comm_assoc
3) ! (r => ! (r | (p & q))) by distr
4) !(! r | ! (r | (p & q))) by impl
5) !(! r | ! r & ! (p & q)) by dm 
6) !!r by simp2
7) r by neg

After the directive (#check tp), george expects the first non-comment line to be the goal of the proof (a line that includes <->). Following this line should be a labelled sequence of proof steps, where each proof step is of the form:

n) formula by rule

The labels must be unique in the proof and can be alphanumeric, but cannot include ".".

The propositional logic rule names used for transformational proof are:

comm_assoc	contr	lem	idemp
impl	contrapos	simp1	simp2
distr	dm	neg	equiv

These are the same names as on your propositional logic transformational proof summary page .

The predicate logic rule names used for transformational proof are:

forall_over_and

exists_over_or

swap_vars

move_exists

move_forall

dm (same name as for prop logic)

These are the same names as on your predicate logic transformational proof summary page .

Here is an example of a the response to a question that requires a transformational proof for predicate logic:

#check TP

! (forall x,y. exists z . P(x,y,z)) <-> exists y,x . forall z . !P(x,y,z)

1) !(forall x,y. exists z . P(x,y,z))
2) exists x . !(forall y. exists z . P(x,y,z))     by dm
3) exists x . exists y. !(exists z . P(x,y,z))     by dm
4) exists y,x . !(exists z . P(x,y,z))        by swap_vars
5) exists y,x . forall z . !P(x,y,z)          by dm

george supports one additional TP rule to allows you make progress on your proof: the ``magic'' rule. The magic rule allows you to conclude any formula at any step in the proof. For example, if you were unable to complete the subproof in the earlier example, you could do:

#check TP

! (r => ! ((p | r) & (r | q))) <->  r

1) ! (r => ! ((p | r) & (r | q)))
2) ! (r => ! ((r | p) & (r | q))) by comm_assoc
3) ! (r => ! (r | (p & q))) by distr
4) !(! r | ! (r | (p & q))) by impl
5) !(! r | ! r & ! (p & q)) by dm 
6) !!r by magic
7) r by neg

What does george check?

For transformational proof, george checks:

• Each formula is syntactically correct.
• Each formula typechecks.
• The rule name is correct.
• The format of the proof is correct.
• Each line has used the rule correctly unless checking times out.
• The line labels are all different.
• The proof matches the goal.