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 on formulas to toggle selection on and off). 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)
Block Language Predicates and Their Standard Interpretation
Tet(a), Cube(a), Dodec(a). Every block is exactly one of these.
Small(a), Medium(a), Large(a). Every block is exactly one of these.
SameSize(a,b). Every block is the SameSize as itself. If SameSize(a,b) then SameSize(b,a). If SameSize(a,b) and SameSize(b,c) then SameSize(a,c).
SameShape(a,b). Every block is the SameShape as itself. If SameShape(a,b) then SameShape(b,a). If SameShape(a,b) and SameShape(b,c) then SameShape(a,c).
Larger(a,b). Not Larger(a,a). If Larger(a,b) then not Larger(b,a). If Larger(a,b) and Larger(b,c) then Larger(a,c). If Smaller(b,a) then Larger(a,b).
Smaller(a,b). Not Smaller(a,a). If Smaller(a,b) then not Smaller(b,a). If Smaller(a,b) and Smaller(b,c) then Smaller(a,c). If Larger(b,a) then Smaller(a,b).
SameCol(a,b). Every block is in the SameCol as itself. If SameCol(a,b) then SameCol(b,a). If SameCol(a,b) and SameCol(b,c) then SameCol(a,c).
SameRow(a,b). Every block is in the SameRow as itself. If SameRow(a,b) then SameRow(b,a). If SameRow(a,b) and SameRow(b,c) then SameRow(a,c).
Adjoins(a,b). Not Adjoins(a,a). If Adjoins(a,b) then Adjoins(b,a).
LeftOf(a,b). Not LeftOf(a,a). If LeftOf(a,b) then not LeftOf(b,a). If LeftOf(a,b) and LeftOf(b,c) then LeftOf(a,c). If RightOf(b,a) then LeftOf(a,b).
RightOf(a,b). Not RightOf(a,a). If RightOf(a,b) then not RightOf(b,a). If RightOf(a,b) and RightOf(b,c) then RightOf(a,c). If LeftOf(b,a) then RightOf(a,b).
FrontOf(a,b). Not FrontOf(a,a). If FrontOf(a,b) then not FrontOf(b,a). If FrontOf(a,b) and FrontOf(b,c) then FrontOf(a,c). If BakcOf(b,a) then FrontOf(a,b).
BackOf(a,b). Not BackOf(a,a). If BackOf(a,b) then not BackOf(b,a). If BackOf(a,b) and BackOf(b,c) then BackOf(a,c). If FrontOf(b,a) then BackOf(a,b).
Between(a,b,c). Not Between(a,a,b). Not Between(a,b,b).
Exercises
[In the widget 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 1)
Close each of the following trees using Ana Con (then Close)