S. Baratella and A. Masini. An approach to infinitary temporal proof theory. Archive for Mathematical Logic, 2004.

Aim of this work is to investigate from a proof-theoretic viewpoint a propositional and a predicate sequent calculus with an omega-type schema of inference that naturally interpret the propositional and the predicate until-free fragments of Linear Time Logic LTL respectively. The two calculi are based on a natural extension of ordinary sequents and of standard modal rules. We examine the pure propositional case (no extralogical axioms), the propositional and the first order predicate cases (both with a possibly infinite set of extralogical axioms). For each system we provide a syntactic proof of cut elimination and a proof of completeness.

[ bib | http ]

Back