|
|
|
|
|
Checking for equality of two DRSs is very useful when generating readings of a sentence. For example, the glue module generates two readings for the sentence John sees Mary:
|
However, it is easy to tell that these two readings are logically the same, and therefore one of them is superfluous. We can use the theorem prover to determine this equivalence, and then delete one of them. A particular theorem prover may be specified, or the argument may be left off to use the default.
|