# Proofs and surfaces

## TL;DR

This paper introduces a formal sequent system for Menelaus' configurations, connecting geometric incidence properties with algebraic structures, and proves its soundness and decidability.

## Contribution

It presents a novel formal sequent system based on 2-cycles of Delta-complexes for Menelaus' configurations, linking geometry with algebraic operad structures.

## Key findings

- The system is sound and decidable.
- Provable sequents yield incidence results.
- A cyclic operad structure is established.

## Abstract

A formal sequent system dealing with Menelaus' configurations is introduced in this paper. The axiomatic sequents of the system stem from 2-cycles of Delta-complexes. The Euclidean and projective interpretations of the sequents are defined and a soundness result is proved. This system is decidable and its provable sequents deliver incidence results. A cyclic operad structure tied to this system is presented by generators and relations.