LP&L Trees 1 Analytical Consequence Ana Con I

Logical System
Last altered 1/9/14


John Barwise and John Etchemendy, [1999] Language, Proof and Logic

LP&L comes with a Normal or Standard Interpretation, and this certainly affects how trees should and can behave.

For example, the polyhedra are either tetrahedra, cubes, or dodecahedra. If a particular polyhedron is a cube it cannot be a tetrahedron, so Cube(a)&Tet(a) cannot be true and a branch containing Cube(a) and Tet(a) should close or be able to close.

One way of doing this is by implementing, for trees, the Fitch linear derivation rule Analytical Consequence or Ana Con (LP&L p.60).

To use Ana Con in a tree you first select one or two formulas in a branch (click to select). 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. Here is a movie showing a simple example



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).

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).




[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 2)

Close each of the following trees using Ana Con (then Close)

Exercise 2 (of 2)
