Analytic sequent calculi with nonlogical axioms

This paper investigates a variety of sequent calculi including substructural ones and calculi with equality that can be used for characterizing AI systems. These calculi have introduction inference rules for logical connectives and contain nonlogical axioms. Nonlogical axioms represent domain knowledge. Derivations in these calculi can be restricted to a normal form and to an ordered form. Inference rules are constrained in these forms. It is proved that these calculi are analytic. Infinite branching can be avoided in inference procedures for these calculi.