Venema, Yde Points, lines and diamonds: A two-sorted modal logic for projective planes. (English) Zbl 0941.03020 J. Log. Comput. 9, No. 5, 601-621 (1999). Summary: We introduce a modal language for talking about projective planes. This language is two-sorted, containing formulas to be evaluated at points and at lines, respectively. The language has two diamonds whose intended accessibility relations are the two directions of the incidence relation between points and lines. We provide a sound and complete axiomatization for the formulas that are valid in the class of projective planes. We also show that it is decidable whether a given formula is satisfiable in a projective plane, and we characterize the computational complexity of this satisfaction problem. Cited in 2 ReviewsCited in 11 Documents MSC: 03B45 Modal logic (including the logic of norms) 51E15 Finite affine and projective planes (geometric aspects) 68T30 Knowledge representation 03B30 Foundations of classical theories (including reverse mathematics) Keywords:modal logic; logic of space; projective geometry; decidability; computational complexity of satisfaction problem; projective planes; axiomatization PDFBibTeX XMLCite \textit{Y. Venema}, J. Log. Comput. 9, No. 5, 601--621 (1999; Zbl 0941.03020) Full Text: DOI