Non-Commutative First-Order Sequent Calculus

Abstract. This paper investigates a non-commutative first-order sequent calculus NCLK. For that, this paper extends a non-commutative positive fragment to a full first-order sequent calculus LK− having antecedent-grouping and no right exchange rule. This paper shows (1) NCLK is equivalent to LJ, (2) NCLK with the exchange rule is equivalent to LK, (3) LK− is equivalent to LJ, and (4) translations between LK− and NCLK.

• Type: Conference
• Year: 2009
• Where: CSL
• Authors: Makoto Tatsuta
• Keywords: Artificial Intelligence, CSL 2009, Sequent Calculus Lk−, Sequent Calculus Nclk, first-order Sequent Calculus