Parts and Overlaps

A logic problem by Adam Richard-Bollans

Your problem is to use first-order logic to represent the following example of reasoning, and use the Prover9 theorem prover to prove that the reasoning is valid.

Use the following template file to create your Prover9 encoding of the problem: parts_and_overlaps.p9

Marks: There are two marks for each sentence, making a total of 10 marks.

Problem Statement

A1	An axiom for Contact: Contact is reflexive.
A2	Definition of Parthood: A region, A, is part of a region, B, if and only if whenever a region, C, is in contact with A then it is in contact with B.
A3	Definition of Proper Parthood: A region A is a proper part of a region B if and only if A is part of B but B is not part of A.
A4	Definition of Overlap: A region A overlaps a region B if and only if there is a region which is part of both region A and B.
Goal	If any region A is a proper part of any region B then A overlaps B and A is in contact with B.

Non-Logical Vocabulary

Predicates: Contact, PartOf, ProperPartOf, Overlaps

Notes:

A1: A relationship is reflexive when it relates elements to themselves. For example = is reflexive as x = x for all x.
The domain is regular regions in space. For those interested in further exploring logical representations of space see Cohn, A. G., Bennett, B., Gooday, J., & Gotts, N. M. (1997). Qualitative spatial representation and reasoning with the region connection calculus. GeoInformatica, 1(3), 275–316.