1/28/2020
Reading
John Barwise and John Etchemendy, [1999] Language, Proof and Logic
What follows are further Ana Con inferences.
To use Ana Con in a tree you first select one or two formula in a branch (click to select or unselect). These formulas will be the premises of your intended inference. Second you choose Ana Con off the menu. It will ask you for your target conclusion, you have to enter that and press Go. If indeed your target conclusion follows, as an analytical consequence, it will be inserted.
The rule Ana Con uses a theorem prover to determine whether your intended conclusion follows from the available premises. It does this by trying to find a proof. Sometimes it will not be able to find a proof even when there is one, this possibility is very rare. The theorem prover is set to try for about 3 seconds of processing time, which is about 30 seconds as you look at it on your computer-- then it will abandon the proof.
Ana Con is typically used in cases involving simple direct inferences from Block Language predicates (LP&L p.22)
Ana Con supports some 'elaborate' inferences, for example
Tet(a),SameShape(a,b) ∴ Tet(b)
Cube(a),SameShape(a,b) ∴ Cube(b)
Dodec(a),SameShape(a,b) ∴ Dodec(b)
Small(a),SameSize(a,b) ∴ Small(b)
Medium(a),SameSize(a,b) ∴ Medium(b)
Large(a),SameSize(a,b) ∴ Large(b)
Smaller(a,b),SameSize(a,c) ∴ Smaller(c,b)
Smaller(a,b),SameSize(b,c) ∴ Smaller(a,c)
Larger(a,b),SameSize(a,c) ∴ Larger(c,b)
Larger(a,b),SameSize(b,c) ∴ Larger(a,c)
FrontOf(a,b),SameRow(b,c) ∴ FrontOf(a,c)
FrontOf(a,b),SameRow(a,c) ∴ FrontOf(c,b)
BackOf(a,b),SameRow(b,c) ∴ BackOf(a,c)
BackOf(a,b),SameRow(a,c) ∴ BackOf(c,b)
LeftOf(a,b),SameCol(b,c) ∴ LeftOf(a,c)
LeftOf(a,b),SameCol(a,c) ∴ LeftOf(c,b)
RightOf(a,b),SameCol(b,c) ∴ RightOf(a,c)
RightOf(a,b),SameCol(a,c) ∴ RightOf(c,b)
Exercises
[In the widgets below:- Click once to select, click again to un-select. Select one item to extend the Tree, select two to close a branch. Select one or two for extending by Analytic Consequence (depending what inference you are trying for). [Select two for extending with identity.]]
Exercise 1 (of 3)
Close each of the following trees using Ana Con (then Close)
Exercise 2 (of 3)
Close each of the following trees using Ana Con (then Close)
Exercise 3 (of 3)
Close each of the following trees using Ana Con (then Close)