george: User Manual

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

Semantic Tableaux Proofs (#check ST)

Here is an example of the response to a question that requires a semantic tableaux proof:

#check ST

p | !q => r, !r |- q

1) p | !q => r
2) !r
3) !q
by imp_br on 1
{
	4) !(p | !q)
	by not_or_nb on 4
	5) !p 
	6) !!q
	closed on  3,6
}
{
	7) r
	closed on 2,7
}

The same directive (#check ST) is used for both propositional and predicate logic semantic tableaux proofs.

After the directive (#check ST), george expects the first non-comment line to be the goal of the proof (a line that includes |-). Following this line should be semantic tableaux proof. The first lines should be a labelled list of the formulas at the root of the tableaux. The line labels can be any string and each formula must be uniquely labelled. The line labels cannot include ".".

Remember that to show an argument is valid, include the negation of the conclusion as a formula at the root of the tableaux.

To use a semantic tableaux to show a set of formulas is inconsistent, use a problem statement of the form a,b,c |- false. Then list the formulas in the set at the root of the tableaux. You do not need to include !false (i.e., the negation of the conclusion) as a formula at the root.

After listing the formulas at the root of the tableaux, there is a line a line describing the rule applied at this moment in the proof in the form:

by rule_name on line_number

or if the branch of the tableaux can be closed at this node, then instead of a rule, use the line:

closed on line_number, line_number

Following the rule, there should be one (for a non-branching rule) or more (for a branching rule) sub-tableauxs, each enclosed within curly braces. A sub-tableaux has a set of formulas at its root followed by a line describing a rule, followed by sub-tableauxs.

Whitespace, such as tabs, is not required but it is recommended for clarity when reading your proof. (Remember the TAs read your proofs!)

Here is a table of the rule names:

Positive	Negative
and_nb	not_and_br
or_br	not_or_nb
imp_br	not_imp_nb
	not_not_nb
iff_br	not_iff_br
forall_nb	not_forall_nb
exists_nb	not_exists_nb

The positive and negative rules for conjunction and disjunction can be used to produce more than two branches (e.g., if there are more than two conjuncts).

These rules are summarized on our summary page on semantic tableaux for propositional logic and our summary page on semantic tableaux for predicate logic .

ST proofs can be constructed incrementally. You can leave a proof without closing all the branches and George will check the correctness of the proof steps included. This is very useful for debugging ST proofs. For example:

#check ST

h => s, r=> !s, h |- !r

1) h => s
2) r=> !s
3) h
4) !!r
by imp_br on 2
{
	5) !r
}
{
	6) !s
}

What does george check?

For semantic tableaux proofs, george checks:

• Each formula is syntactically correct.
• Each formula typechecks.
• The name of each proof rule is a valid rule.
• The format of the proof is correct, including that the line numbers are unique.
• The proof rule has been correctly applied. This includes checking that the line number the rule uses are the correct ones and formulas derived from the rule are correct.

If george encounters an error in the proof, it provides you with feedback and then continues its correctness analysis as if the incorrect line had been correct in order to provide you with as much feedback as possible.