An approach to infinitary temporal proof theory |
| |
Authors: | Stefano?Baratella Email author" target="_blank">Andrea?MasiniEmail author |
| |
Institution: | (1) Dipartimento di Matematica, Università di Trento, via Sommarive 14, 38050 Povo, TN, Italy;(2) Dipartimento di Informatica, Università di Verona strada le Grazie 15, Ca Vignal 2, 37124 Verona, Italy |
| |
Abstract: | Aim of this work is to investigate from a proof-theoretic viewpoint a propositional and a predicate sequent calculus with an –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.Supported by MIUR COFIN 02 Teoria dei Modelli e Teoria degli Insiemi, loro interazioni ed applicazioni.Supported by MIUR COFIN 02 PROTOCOLLO.Mathematics Subject Classification (2000):03B22, 03B45, 03F05 |
| |
Keywords: | Proof theory Sequent calculus Infinitary logic Cut elimination Modal logic |
本文献已被 SpringerLink 等数据库收录! |
|