# Logic & Lambda Calculus

The nltk.logic package allows expressions of First-Order Logic (FOL) to be parsed into Expression objects. In addition to FOL, the parser handles lambda-abstraction with variables of higher order.

# Overview

```>>> from nltk.sem.logic import *
```

The default inventory of logical constants is the following:

```>>> boolean_ops() # doctest: +NORMALIZE_WHITESPACE
negation           -
conjunction        &
disjunction        |
implication        ->
equivalence        <->
>>> equality_preds() # doctest: +NORMALIZE_WHITESPACE
equality           =
inequality         !=
>>> binding_ops() # doctest: +NORMALIZE_WHITESPACE
existential        exists
universal          all
lambda             \
```

# Regression Tests

## Untyped Logic

Process logical expressions conveniently:

```>>> read_expr = Expression.fromstring
```

### Test for equality under alpha-conversion

```>>> e1 = read_expr('exists x.P(x)')
>>> print(e1)
exists x.P(x)
>>> e2 = e1.alpha_convert(Variable('z'))
>>> print(e2)
exists z.P(z)
>>> e1 == e2
True
```
```>>> l = read_expr(r'\X.\X.X(X)(1)').simplify()
>>> l == id
True
```

### Test numerals

```>>> zero = read_expr(r'\F x.x')
>>> succ = read_expr(r'\N F x.F(N(F,x))')
>>> plus = read_expr(r'\M N F x.M(F,N(F,x))')
>>> mult = read_expr(r'\M N F.M(N(F))')
>>> pred = read_expr(r'\N F x.(N(\G H.H(G(F)))(\u.x)(\u.u))')
>>> v1 = ApplicationExpression(succ, zero).simplify()
>>> v1 == one
True
>>> v2 = ApplicationExpression(succ, v1).simplify()
>>> v2 == two
True
>>> v3 = ApplicationExpression(ApplicationExpression(plus, v1), v2).simplify()
>>> v3 == three
True
>>> v4 = ApplicationExpression(ApplicationExpression(mult, v2), v2).simplify()
>>> v4 == four
True
>>> v5 = ApplicationExpression(pred, ApplicationExpression(pred, v4)).simplify()
>>> v5 == two
True
```

Overloaded operators also exist, for convenience.

```>>> print(succ(zero).simplify() == one)
True
>>> print(plus(one,two).simplify() == three)
True
>>> print(mult(two,two).simplify() == four)
True
>>> print(pred(pred(four)).simplify() == two)
True
```
```>>> john = read_expr(r'john')
>>> man(john).simplify()
<ApplicationExpression man(john)>
>>> print(-walk(john).simplify())
-walk(john)
>>> print((man(john) & walk(john)).simplify())
(man(john) & walk(john))
>>> print((man(john) | walk(john)).simplify())
(man(john) | walk(john))
>>> print((man(john) > walk(john)).simplify())
(man(john) -> walk(john))
>>> print((man(john) < walk(john)).simplify())
(man(john) <-> walk(john))
```

Python's built-in lambda operator can also be used with Expressions

```>>> john = VariableExpression(Variable('john'))
>>> run_var = VariableExpression(Variable('run'))
>>> run = lambda x: run_var(x)
>>> run(john)
<ApplicationExpression run(john)>
```

#### betaConversionTestSuite.pl

Tests based on Blackburn & Bos' book, Representation and Inference for Natural Language.

```>>> x1 = read_expr(r'\P.P(mia)(\x.walk(x))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'exists x.(man(x) & ((\P.exists x.(woman(x) & P(x)))(\y.love(x,y))))').simplify()
>>> x2 = read_expr(r'exists x.(man(x) & exists y.(woman(y) & love(x,y)))').simplify()
>>> x1 == x2
True
>>> x1 == x2
True
>>> x1 == x2
True
>>> x1 == x2
True
>>> x1 = read_expr(r'\a.((\b.like(b,a)(vincent)) & sleep(a))').simplify()
>>> x2 = read_expr(r'\a.(like(vincent,a) & sleep(a))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'(\a.\b.like(b,a)(mia)(vincent))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'P((\a.sleep(a)(vincent)))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'\A.A((\b.sleep(b)(vincent)))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'\A.A(sleep(vincent))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'(\A.A(vincent)(\b.sleep(b)))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'\A.believe(mia,A(vincent))(\b.sleep(b))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'(\A.(A(vincent) & A(mia)))(\b.sleep(b))').simplify()
>>> x2 = read_expr(r'(sleep(vincent) & sleep(mia))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'\A.\B.(\C.C(A(vincent))(\d.probably(d)) & (\C.C(B(mia))(\d.improbably(d))))(\f.walk(f))(\f.talk(f))').simplify()
>>> x2 = read_expr(r'(probably(walk(vincent)) & improbably(talk(mia)))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'(\a.\b.(\C.C(a,b)(\d.\f.love(d,f))))(jules)(mia)').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'(\A.\B.exists c.(A(c) & B(c)))(\d.boxer(d),\d.sleep(d))').simplify()
>>> x2 = read_expr(r'exists c.(boxer(c) & sleep(c))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'\A.Z(A)(\c.\a.like(a,c))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'\A.\b.A(b)(\c.\b.like(b,c))').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'(\a.\b.(\C.C(a,b)(\b.\a.loves(b,a))))(jules)(mia)').simplify()
>>> x1 == x2
True
```
```>>> x1 = read_expr(r'(\A.\b.(exists b.A(b) & A(b)))(\c.boxer(c))(vincent)').simplify()
>>> x2 = read_expr(r'((exists b.boxer(b)) & boxer(vincent))').simplify()
>>> x1 == x2
True
```

### Test Parser

```>>> print(read_expr(r'john'))
john
x
-man(x)
--man(x)
man(x)
man(x)
(man(x) <-> tall(x))
(man(x) <-> tall(x))
>>> print(read_expr(r'(man(x) & tall(x) & walks(x))'))
(man(x) & tall(x) & walks(x))
>>> print(read_expr(r'(man(x) & tall(x) & walks(x))').first)
(man(x) & tall(x))
>>> print(read_expr(r'man(x) | tall(x) & walks(x)'))
(man(x) | (tall(x) & walks(x)))
>>> print(read_expr(r'((man(x) & tall(x)) | walks(x))'))
((man(x) & tall(x)) | walks(x))
>>> print(read_expr(r'man(x) & (tall(x) | walks(x))'))
(man(x) & (tall(x) | walks(x)))
>>> print(read_expr(r'(man(x) & (tall(x) | walks(x)))'))
(man(x) & (tall(x) | walks(x)))
>>> print(read_expr(r'P(x) -> Q(x) <-> R(x) | S(x) & T(x)'))
((P(x) -> Q(x)) <-> (R(x) | (S(x) & T(x))))
exists x.man(x)
exists x.(man(x) & tall(x))
>>> print(read_expr(r'exists x.(man(x) & tall(x) & walks(x))'))
exists x.(man(x) & tall(x) & walks(x))
(-P(x) & Q(x))
True
\x.man(x)
\x.man(x)(john)
(\x.man(x)(john) & tall(x))
\x y.sees(x,y)
\x y.sees(x,y)
(\x y.sees(x,y))(a)
(\x y.sees(x,y))(a)
((\x y.sees(x,y))(a))(b)
((\x y.sees(x,y))(a))(b)
((\x y.sees(x,y))(a))(b)
((\x y.sees(x,y))(a))(b)
((\x y.sees(x,y))(a))(b)
P(x,y,z)
P(Q)
P(Q(x))
(\x.exists y.walks(x,y))(x)
exists x.(x = john)
((\P Q.exists x.(P(x) & Q(x)))(\x.dog(x)))(\x.bark(x))
>>> a = read_expr(r'exists c.exists b.A(b,c) & A(b,c)')
>>> b = read_expr(r'(exists c.(exists b.A(b,c))) & A(b,c)')
>>> print(a == b)
True
>>> a = read_expr(r'exists c.(exists b.A(b,c) & A(b,c))')
>>> b = read_expr(r'exists c.((exists b.A(b,c)) & A(b,c))')
>>> print(a == b)
True
exists x.(x = y)
A(B,C)
A(B,C)
A(B(C))
A(B(C))
A(B(C))
A(B(C))
-(A = B)
>>> print(read_expr('P(x) & x=y & P(y)'))
(P(x) & (x = y) & P(y))
... except LogicalExpressionException as e: print(e)
'walk' is an illegal variable name.  Constants may not be abstracted.
\walk.walk(x)
^
... except LogicalExpressionException as e: print(e)
'walk' is an illegal variable name.  Constants may not be quantified.
all walk.walk(john)
^
... except LogicalExpressionException as e: print(e)
'x' is an illegal predicate name.  Individual variables may not be used as predicates.
x(john)
^
```
```>>> from nltk.sem.logic import LogicParser # hack to give access to custom quote chars
>>> lpq = LogicParser()
>>> lpq.quote_chars = [("'", "'", "\\", False)]
>>> print(lpq.parse(r"(man(x) & 'tall\'s,' (x) & walks (x) )"))
(man(x) & tall's,(x) & walks(x))
>>> lpq.quote_chars = [("'", "'", "\\", True)]
>>> print(lpq.parse(r"'tall\'s,'"))
'tall\'s,'
>>> print(lpq.parse(r"'spaced name(x)'"))
'spaced name(x)'
>>> print(lpq.parse(r"-'tall\'s,'(x)"))
-'tall\'s,'(x)
>>> print(lpq.parse(r"(man(x) & 'tall\'s,' (x) & walks (x) )"))
(man(x) & 'tall\'s,'(x) & walks(x))
```

### Simplify

```>>> print(read_expr(r'\x.man(x)(john)').simplify())
man(john)
man(john)
sees(john,mary)
sees(john,mary)
sees(john,mary)
sees(john,mary)
\y.sees(john,y)
\y.sees(john,y)
sees(john,mary)
sees(john,mary)
>>> print(read_expr(r'exists x.(man(x) & (\x.exists y.walks(x,y))(x))').simplify())
exists x.(man(x) & exists y.walks(x,y))
>>> e1 = read_expr(r'exists x.(man(x) & (\x.exists y.walks(x,y))(y))').simplify()
>>> e2 = read_expr(r'exists x.(man(x) & exists z1.walks(y,z1))')
>>> e1 == e2
True
>>> print(read_expr(r'(\P Q.exists x.(P(x) & Q(x)))(\x.dog(x))').simplify())
\Q.exists x.(dog(x) & Q(x))
exists x.(dog(x) & bark(x))
Q(x,y)
```

### Replace

```>>> a = read_expr(r'a')
```
```>>> print(read_expr(r'man(x)').replace(x.variable, a, False))
man(a)
>>> print(read_expr(r'(man(x) & tall(x))').replace(x.variable, a, False))
(man(a) & tall(a))
exists x.man(x)
exists a.man(a)
exists x.give(x,a,z)
exists x.give(x,a,z)
>>> e1 = read_expr(r'exists x.give(x,y,z)').replace(y.variable, x, False)
>>> e1 == e2
True
>>> e1 = read_expr(r'exists x.give(x,y,z)').replace(y.variable, x, True)
>>> e1 == e2
True
>>> print(read_expr(r'\x y z.give(x,y,z)').replace(y.variable, a, False))
\x y z.give(x,y,z)
>>> print(read_expr(r'\x y z.give(x,y,z)').replace(y.variable, a, True))
\x a z.give(x,a,z)
\x y.give(x,y,a)
\x y.give(x,y,a)
>>> e1 = read_expr(r'\x.\y.give(x,y,z)').replace(z.variable, x, False)
>>> e1 == e2
True
>>> e1 = read_expr(r'\x.\y.give(x,y,z)').replace(z.variable, x, True)
>>> e1 == e2
True
\x.give(x,y,y)
\x.give(x,y,y)
```
```>>> from nltk.sem import logic
>>> logic._counter._value = 0
>>> print(read_expr('exists e1 e2.(walk(e1) & talk(e2))').replace(e1.variable, e2, True))
exists e2 e01.(walk(e2) & talk(e01))
```

### Variables / Free

```>>> examples = [r'walk(john)',
...             r'walk(x)',
...             r'?vp(?np)',
...             r'see(john,mary)',
...             r'exists x.walk(x)',
...             r'\x.see(john,x)',
...             r'\x.see(john,x)(mary)',
...             r'P(x)',
...             r'\P.P(x)',
...             r'aa(x,bb(y),cc(z),P(w),u)',
...             r'bo(?det(?n),@x)']
>>> examples = [read_expr(e) for e in examples]
```
```>>> for e in examples:
...     print('%-25s' % e, sorted(e.free()))
walk(john)                []
walk(x)                   [Variable('x')]
?vp(?np)                  []
see(john,mary)            []
exists x.walk(x)          []
\x.see(john,x)            []
(\x.see(john,x))(mary)    []
P(x)                      [Variable('P'), Variable('x')]
\P.P(x)                   [Variable('x')]
aa(x,bb(y),cc(z),P(w),u)  [Variable('P'), Variable('u'), Variable('w'), Variable('x'), Variable('y'), Variable('z')]
bo(?det(?n),@x)           []
```
```>>> for e in examples:
...     print('%-25s' % e, sorted(e.constants()))
walk(john)                [Variable('john')]
walk(x)                   []
?vp(?np)                  [Variable('?np')]
see(john,mary)            [Variable('john'), Variable('mary')]
exists x.walk(x)          []
\x.see(john,x)            [Variable('john')]
(\x.see(john,x))(mary)    [Variable('john'), Variable('mary')]
P(x)                      []
\P.P(x)                   []
aa(x,bb(y),cc(z),P(w),u)  []
bo(?det(?n),@x)           [Variable('?n'), Variable('@x')]
```
```>>> for e in examples:
...     print('%-25s' % e, sorted(e.predicates()))
walk(john)                [Variable('walk')]
walk(x)                   [Variable('walk')]
?vp(?np)                  [Variable('?vp')]
see(john,mary)            [Variable('see')]
exists x.walk(x)          [Variable('walk')]
\x.see(john,x)            [Variable('see')]
(\x.see(john,x))(mary)    [Variable('see')]
P(x)                      []
\P.P(x)                   []
aa(x,bb(y),cc(z),P(w),u)  [Variable('aa'), Variable('bb'), Variable('cc')]
bo(?det(?n),@x)           [Variable('?det'), Variable('bo')]
```
```>>> for e in examples:
...     print('%-25s' % e, sorted(e.variables()))
walk(john)                []
walk(x)                   [Variable('x')]
?vp(?np)                  [Variable('?np'), Variable('?vp')]
see(john,mary)            []
exists x.walk(x)          []
\x.see(john,x)            []
(\x.see(john,x))(mary)    []
P(x)                      [Variable('P'), Variable('x')]
\P.P(x)                   [Variable('x')]
aa(x,bb(y),cc(z),P(w),u)  [Variable('P'), Variable('u'), Variable('w'), Variable('x'), Variable('y'), Variable('z')]
bo(?det(?n),@x)           [Variable('?det'), Variable('?n'), Variable('@x')]
```
normalize
```>>> print(read_expr(r'\e083.(walk(e083, z472) & talk(e092, z938))').normalize())
\e01.(walk(e01,z3) & talk(e02,z4))
```

## Typed Logic

```>>> from nltk.sem.logic import LogicParser
>>> tlp = LogicParser(True)
>>> print(tlp.parse(r'man(x)').type)
?
>>> print(tlp.parse(r'walk(angus)').type)
?
>>> print(tlp.parse(r'-man(x)').type)
t
>>> print(tlp.parse(r'(man(x) <-> tall(x))').type)
t
>>> print(tlp.parse(r'exists x.(man(x) & tall(x))').type)
t
>>> print(tlp.parse(r'\x.man(x)').type)
<e,?>
>>> print(tlp.parse(r'john').type)
e
>>> print(tlp.parse(r'\x y.sees(x,y)').type)
<e,<e,?>>
>>> print(tlp.parse(r'\x.man(x)(john)').type)
?
>>> print(tlp.parse(r'\x.\y.sees(x,y)(john)').type)
<e,?>
>>> print(tlp.parse(r'\x.\y.sees(x,y)(john)(mary)').type)
?
>>> print(tlp.parse(r'\P.\Q.exists x.(P(x) & Q(x))').type)
<<e,t>,<<e,t>,t>>
>>> print(tlp.parse(r'\x.y').type)
<?,e>
>>> print(tlp.parse(r'\P.P(x)').type)
<<e,?>,?>
```
```>>> parsed = tlp.parse('see(john,mary)')
>>> print(parsed.type)
?
>>> print(parsed.function)
see(john)
>>> print(parsed.function.type)
<e,?>
>>> print(parsed.function.function)
see
>>> print(parsed.function.function.type)
<e,<e,?>>
```
```>>> parsed = tlp.parse('P(x,y)')
>>> print(parsed)
P(x,y)
>>> print(parsed.type)
?
>>> print(parsed.function)
P(x)
>>> print(parsed.function.type)
<e,?>
>>> print(parsed.function.function)
P
>>> print(parsed.function.function.type)
<e,<e,?>>
```
```>>> print(tlp.parse(r'P').type)
?
```
```>>> print(tlp.parse(r'P', {'P': 't'}).type)
t
```
```>>> a = tlp.parse(r'P(x)')
>>> print(a.type)
?
>>> print(a.function.type)
<e,?>
>>> print(a.argument.type)
e
```
```>>> a = tlp.parse(r'-P(x)')
>>> print(a.type)
t
>>> print(a.term.type)
t
>>> print(a.term.function.type)
<e,t>
>>> print(a.term.argument.type)
e
```
```>>> a = tlp.parse(r'P & Q')
>>> print(a.type)
t
>>> print(a.first.type)
t
>>> print(a.second.type)
t
```
```>>> a = tlp.parse(r'(P(x) & Q(x))')
>>> print(a.type)
t
>>> print(a.first.type)
t
>>> print(a.first.function.type)
<e,t>
>>> print(a.first.argument.type)
e
>>> print(a.second.type)
t
>>> print(a.second.function.type)
<e,t>
>>> print(a.second.argument.type)
e
```
```>>> a = tlp.parse(r'\x.P(x)')
>>> print(a.type)
<e,?>
>>> print(a.term.function.type)
<e,?>
>>> print(a.term.argument.type)
e
```
```>>> a = tlp.parse(r'\P.P(x)')
>>> print(a.type)
<<e,?>,?>
>>> print(a.term.function.type)
<e,?>
>>> print(a.term.argument.type)
e
```
```>>> a = tlp.parse(r'(\x.P(x)(john)) & Q(x)')
>>> print(a.type)
t
>>> print(a.first.type)
t
>>> print(a.first.function.type)
<e,t>
>>> print(a.first.function.term.function.type)
<e,t>
>>> print(a.first.function.term.argument.type)
e
>>> print(a.first.argument.type)
e
```
```>>> a = tlp.parse(r'\x y.P(x,y)(john)(mary) & Q(x)')
>>> print(a.type)
t
>>> print(a.first.type)
t
>>> print(a.first.function.type)
<e,t>
>>> print(a.first.function.function.type)
<e,<e,t>>
```
```>>> a = tlp.parse(r'--P')
>>> print(a.type)
t
>>> print(a.term.type)
t
>>> print(a.term.term.type)
t
```
```>>> tlp.parse(r'\x y.P(x,y)').type
<e,<e,?>>
>>> tlp.parse(r'\x y.P(x,y)', {'P': '<e,<e,t>>'}).type
<e,<e,t>>
```
```>>> a = tlp.parse(r'\P y.P(john,y)(\x y.see(x,y))')
>>> a.type
<e,?>
>>> a.function.type
<<e,<e,?>>,<e,?>>
>>> a.function.term.term.function.function.type
<e,<e,?>>
>>> a.argument.type
<e,<e,?>>
```
```>>> a = tlp.parse(r'exists c f.(father(c) = f)')
>>> a.type
t
>>> a.term.term.type
t
>>> a.term.term.first.type
e
>>> a.term.term.first.function.type
<e,e>
>>> a.term.term.second.type
e
```

typecheck()

```>>> a = tlp.parse('P(x)')
>>> b = tlp.parse('Q(x)')
>>> a.type
?
>>> c = a & b
>>> c.first.type
?
>>> c.typecheck() # doctest: +ELLIPSIS
{...}
>>> c.first.type
t
```
```>>> a = tlp.parse('P(x)')
>>> b = tlp.parse('P(x) & Q(x)')
>>> a.type
?
>>> typecheck([a,b]) # doctest: +ELLIPSIS
{...}
>>> a.type
t
```
```>>> e = tlp.parse(r'man(x)')
>>> print(dict((k,str(v)) for k,v in e.typecheck().items()) == {'x': 'e', 'man': '<e,?>'})
True
>>> sig = {'man': '<e, t>'}
>>> e = tlp.parse(r'man(x)', sig)
>>> print(e.function.type)
<e,t>
>>> print(dict((k,str(v)) for k,v in e.typecheck().items()) == {'x': 'e', 'man': '<e,t>'})
True
>>> print(e.function.type)
<e,t>
>>> print(dict((k,str(v)) for k,v in e.typecheck(sig).items()) == {'x': 'e', 'man': '<e,t>'})
True
```

findtype()

```>>> print(tlp.parse(r'man(x)').findtype(Variable('man')))
<e,?>
>>> print(tlp.parse(r'see(x,y)').findtype(Variable('see')))
<e,<e,?>>
>>> print(tlp.parse(r'P(Q(R(x)))').findtype(Variable('Q')))
?
```

```>>> Type.fromstring('e')
e
>>> Type.fromstring('<e,t>')
<e,t>
>>> Type.fromstring('<<e,t>,<e,t>>')
<<e,t>,<e,t>>
>>> Type.fromstring('<<e,?>,?>')
<<e,?>,?>
```

alternative type format

```>>> Type.fromstring('e').str()
'IND'
>>> Type.fromstring('<e,?>').str()
'(IND -> ANY)'
>>> Type.fromstring('<<e,t>,t>').str()
'((IND -> BOOL) -> BOOL)'
```

Type.__eq__()

```>>> from nltk.sem.logic import *
```
```>>> e = ENTITY_TYPE
>>> t = TRUTH_TYPE
>>> a = ANY_TYPE
>>> et = ComplexType(e,t)
>>> eet = ComplexType(e,ComplexType(e,t))
>>> at = ComplexType(a,t)
>>> ea = ComplexType(e,a)
>>> aa = ComplexType(a,a)
```
```>>> e == e
True
>>> t == t
True
>>> e == t
False
>>> a == t
False
>>> t == a
False
>>> a == a
True
>>> et == et
True
>>> a == et
False
>>> et == a
False
>>> a == ComplexType(a,aa)
True
>>> ComplexType(a,aa) == a
True
```

matches()

```>>> e.matches(t)
False
>>> a.matches(t)
True
>>> t.matches(a)
True
>>> a.matches(et)
True
>>> et.matches(a)
True
>>> ea.matches(eet)
True
>>> eet.matches(ea)
True
>>> aa.matches(et)
True
>>> aa.matches(t)
True
```

### Type error during parsing

```>>> try: print(tlp.parse(r'exists x y.(P(x) & P(x,y))'))
... except InconsistentTypeHierarchyException as e: print(e)
The variable 'P' was found in multiple places with different types.
>>> try: tlp.parse(r'\x y.see(x,y)(\x.man(x))')
... except TypeException as e: print(e)
The function '\x y.see(x,y)' is of type '<e,<e,?>>' and cannot be applied to '\x.man(x)' of type '<e,?>'.  Its argument must match type 'e'.
>>> try: tlp.parse(r'\P x y.-P(x,y)(\x.-man(x))')
... except TypeException as e: print(e)
The function '\P x y.-P(x,y)' is of type '<<e,<e,t>>,<e,<e,t>>>' and cannot be applied to '\x.-man(x)' of type '<e,t>'.  Its argument must match type '<e,<e,t>>'.
```
```>>> a = tlp.parse(r'-talk(x)')
>>> signature = a.typecheck()
>>> try: print(tlp.parse(r'-talk(x,y)', signature))
... except InconsistentTypeHierarchyException as e: print(e)
The variable 'talk' was found in multiple places with different types.
```
```>>> a = tlp.parse(r'-P(x)')
>>> b = tlp.parse(r'-P(x,y)')
>>> a.typecheck() # doctest: +ELLIPSIS
{...}
>>> b.typecheck() # doctest: +ELLIPSIS
{...}
>>> try: typecheck([a,b])
... except InconsistentTypeHierarchyException as e: print(e)
The variable 'P' was found in multiple places with different types.
```
```>>> a = tlp.parse(r'P(x)')
>>> b = tlp.parse(r'P(x,y)')
>>> signature = {'P': '<e,t>'}
>>> a.typecheck(signature) # doctest: +ELLIPSIS
{...}
>>> try: typecheck([a,b], signature)
... except InconsistentTypeHierarchyException as e: print(e)
The variable 'P' was found in multiple places with different types.
```

### Parse errors

```>>> try: read_expr(r'')
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
<BLANKLINE>
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
(
^
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
)
^
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
()
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expected token ')'.
(P(x) & Q(x)
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
(P(x) &
^
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
(P(x) | )
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
P(x) ->
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expected token ')'.
P(x
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
P(x,
^
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
P(x,)
^
... except LogicalExpressionException as e: print(e)
End of input found.  Variable and Expression expected following quantifier 'exists'.
exists
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
exists x
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
exists x.
^
... except LogicalExpressionException as e: print(e)
End of input found.  Variable and Expression expected following lambda operator.
\
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
\ x
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
\ x y
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
\ x.
^
... except LogicalExpressionException as e: print(e)
Unexpected token: 'Q'.
P(x)Q(x)
^
... except LogicalExpressionException as e: print(e)
Unexpected token: 'Q'.  Expected token ')'.
(P(x)Q(x)
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
exists x y
^
... except LogicalExpressionException as e: print(e)
End of input found.  Expression expected.
exists x y.
^
>>> try: read_expr(r'exists x -> y')
... except LogicalExpressionException as e: print(e)
Unexpected token: '->'.  Expression expected.
exists x -> y
^
```
```>>> try: read_expr(r'A -> ((P(x) & Q(x)) -> Z')
... except LogicalExpressionException as e: print(e)
End of input found.  Expected token ')'.
A -> ((P(x) & Q(x)) -> Z
^
>>> try: read_expr(r'A -> ((P(x) &) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> ((P(x) &) -> Z
^
>>> try: read_expr(r'A -> ((P(x) | )) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> ((P(x) | )) -> Z
^
>>> try: read_expr(r'A -> (P(x) ->) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (P(x) ->) -> Z
^
>>> try: read_expr(r'A -> (P(x) -> Z')
... except LogicalExpressionException as e: print(e)
End of input found.  Expected token ')'.
A -> (P(x) -> Z
^
>>> try: read_expr(r'A -> (P(x,) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (P(x,) -> Z
^
>>> try: read_expr(r'A -> (P(x,)) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (P(x,)) -> Z
^
>>> try: read_expr(r'A -> (exists) -> Z')
... except LogicalExpressionException as e: print(e)
')' is an illegal variable name.  Constants may not be quantified.
A -> (exists) -> Z
^
>>> try: read_expr(r'A -> (exists x) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (exists x) -> Z
^
>>> try: read_expr(r'A -> (exists x.) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (exists x.) -> Z
^
>>> try: read_expr(r'A -> (\  ) -> Z')
... except LogicalExpressionException as e: print(e)
')' is an illegal variable name.  Constants may not be abstracted.
A -> (\  ) -> Z
^
>>> try: read_expr(r'A -> (\ x) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (\ x) -> Z
^
>>> try: read_expr(r'A -> (\ x y) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (\ x y) -> Z
^
>>> try: read_expr(r'A -> (\ x.) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (\ x.) -> Z
^
>>> try: read_expr(r'A -> (P(x)Q(x)) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: 'Q'.  Expected token ')'.
A -> (P(x)Q(x)) -> Z
^
>>> try: read_expr(r'A -> ((P(x)Q(x)) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: 'Q'.  Expected token ')'.
A -> ((P(x)Q(x)) -> Z
^
>>> try: read_expr(r'A -> (all x y) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (all x y) -> Z
^
>>> try: read_expr(r'A -> (exists x y.) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: ')'.  Expression expected.
A -> (exists x y.) -> Z
^
>>> try: read_expr(r'A -> (exists x -> y) -> Z')
... except LogicalExpressionException as e: print(e)
Unexpected token: '->'.  Expression expected.
A -> (exists x -> y) -> Z
^
```