Foundations for an Abstract Proof Theory in the Context of Horn Rules

Tim LyonTim Lyon, Piotr Ostropolski-NalewajaPiotr Ostropolski-Nalewaja

Tim Lyon, Piotr Ostropolski-Nalewaja
Foundations for an Abstract Proof Theory in the Context of Horn Rules
ACM Transactions on Computational Logic, to appear

Details
Bibtex

KurzfassungAbstract
We introduce a novel, logic-independent framework for the study of sequent-style proof systems, which covers a number of proof-theoretic formalisms and concrete proof systems that appear in the literature. In particular, we introduce a generalized form of sequents, dubbed "g-sequents," which are taken to be binary graphs of typical, Gentzen-style sequents. We then define a variety of inference rule types as sets of operations that act over such objects, and define abstract (sequent) calculi as pairs consisting of a set of g-sequents together with a finite set of operations. Our approach permits an analysis of how certain inference rule types interact in a general setting, demonstrating under what conditions rules of a specific type can be permuted with or simulated by others, and being applicable to any multisequent proof system that fits within our framework. We then leverage our permutation and simulation results to establish generic calculus and proof transformation algorithms, which show that every abstract calculus can be effectively transformed into a lattice of polynomially equivalent abstract calculi. We determine the complexity of computing this lattice and compute the relative sizes of proofs and sequents within distinct calculi of a lattice. We recognize that top and bottom elements in lattices correspond to many known deep-inference nested sequent systems and labeled sequent systems (respectively) for logics characterized by Horn properties.
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@article{LO2026,
  author  = {Tim Lyon and Piotr Ostropolski-Nalewaja},
  title   = {Foundations for an Abstract Proof Theory in the Context of Horn
             Rules},
  journal = {ACM Transactions on Computational Logic},
  year    = {2026},
  month   = {June}
}