Name
Abstract | ||
|---|---|---|
We formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We prove soundness and completeness over relational and trace models. As a corollary, we obtain a complete sequent calculus for inclusion and equivalence of regular expressions. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1145/772062.772066 | ACM Trans. Comput. Log. |
Keywords | Field | DocType |
dynamic logic,linear logic,hoare logic,noncommutative sequent calculus,trace model,substructural logic,regular expression,kleene algebra,sequent calculus,complete sequent calculus,intuitionistic linear implication,specification,propositional hoare logic,kleene algebra with tests,partial correctness,partial correctness assertion | Discrete mathematics,Algebra,Natural deduction,Hoare logic,Sequent calculus,Substructural logic,Noncommutative logic,Sequent,Linear logic,Cut-elimination theorem,Mathematics | Journal |
Volume | Issue | Citations |
4 | 3 | 11 |
PageRank | References | Authors |
0.69 | 15 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dexter C. Kozen | 1 | 5108 | 912.56 |
| Jerzy Tiuryn | 2 | 1210 | 126.00 |