Name
Abstract | ||
|---|---|---|
Sequent calculi usually provide a general deductive setting that uniformly embeds other proof-theoretical approaches, such as tableaux methods, resolution techniques, goal-directed proofs, etc. Unfortunately, in temporal logic, existing sequent calculi make use of a kind of inference rules that prevent the effective mechanization of temporal deduction in the general setting. In particular, temporal sequent calculi either need some form of cut, or they make use of invariants, or they include infinitary rules. This is the case even for the simplest kind of temporal logic, propositional linear temporal logic (PLTL). In this paper, we provide a complete finitary sequent calculus for PLTL, called FC, that not only is cut-free but also invariant-free. In particular, we introduce new rules which provide a new style of temporal deduction. We give a detailed proof of completeness. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-74915-8_36 | CSL |
Keywords | Field | DocType |
temporal sequent calculus,temporal logic,temporal deduction,invariant-free sequent calculus,existing sequent,new rule,complete finitary sequent calculus,sequent calculus,general setting,propositional linear temporal logic,general deductive,linear temporal logic,inference rule | Discrete mathematics,Natural deduction,Computer science,Proof calculus,Sequent calculus,Noncommutative logic,Sequent,Cut-elimination theorem,Rule of inference,Curry–Howard correspondence | Conference |
Volume | ISSN | ISBN |
4646 | 0302-9743 | 3-540-74914-4 |
Citations | PageRank | References |
9 | 0.77 | 9 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Joxe Gaintzarain | 1 | 9 | 0.77 |
| Montserrat Hermo | 2 | 55 | 10.77 |
| Paqui Lucio | 3 | 102 | 19.66 |
| Marisa Navarro | 4 | 158 | 28.20 |
| Fernando Orejas | 5 | 942 | 113.72 |