An Axiom System for a Spatial Logic with Convexity
Adam Trybus · Frontiers in artificial intelligence and applications · 2010
This paper presents a part of work in progress on axiomatizing a spatial logic with convexity and inclusion predicates (hereinafter called convexity logic), with some intended interpretation over the real plane. More formally, let Lconv,≤be a language of first order logic and two non-logical primitives: conv (interpreted as a property of a set of being convex) and ≤ (interpreted as the set inclusion relation). We let variables range over regular open rational polygons in the real plane (denoted ROQ(R2)). We call the tuple M = ⟨ROQ, conv, ≤⟩ — where primitives are defined as indicated above — a standard model. We propose an axiomatization of the theory of M and prove soundness and completeness for this axiomatization.