## 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

*This file has been generated by
bibtex2html 1.60*
>>> BackToHomePage(Protocollo) <<<