Nowadays there is a large number of non-classical logics, each one best suited for reasoning about some issues in abstract fields, such as linguistics or epistemology, among others. Proving interesting properties for each one of them supposes a big workload for logicians and computer scientists. We want an approach into this problematic that is modular. To adress this issue, the report shows new insights in the construction of Atomic Logics introduced by Guillaume Aucher. Atomic Logics let us represent very general left and right introduction rules and they come along a new kind of rules based on display logics and residuation. A new approach is taken into the definition of Atomic Logics, which is now built on a class of actions for which we prove cut-elimination. We show that some of them are equivalent to Aucher's Atomic Logics and we prove cut-elimination and Craig Interpolation for a class of them. The introduced theory is applied to the non-associative Lambek Calculus throughout the report. It is accompanied by a computer-checked formalisation of the original syntax in the proof assistant Coq.

翻译：当前存在大量非经典逻辑，每种逻辑都最适合在抽象领域（如语言学或认识论等）中推理特定问题。为每种逻辑证明有趣的性质对逻辑学家和计算机科学家而言意味着巨大的工作量。我们希望采用一种模块化的方法来解决这一问题。为应对这一挑战，本报告展示了Guillaume Aucher提出的原子逻辑构建中的新见解。原子逻辑使我们能够表示非常一般的左、右引入规则，并伴随一种基于显示逻辑和剩余原则的新规则。本文采用了定义原子逻辑的新方法，该方法建立在某类行为之上，并对其证明了消割定理。我们表明这些行为中的一部分与Aucher的原子逻辑等价，并对其中的一类证明了消割定理和Craig插值性质。本报告将所引入的理论应用于非结合Lambek演算，并在证明助手Coq中附带了原始语法的计算机验证形式化。