DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2023.5

A Cyclic Proof System for Full Computation Tree Logic

Authors: Bahareh Afshari, Graham E. Leigh, and Guillermo Menéndez Turata

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract

Full Computation Tree Logic, commonly denoted CTL*, is the extension of Linear Temporal Logic LTL by path quantification for reasoning about branching time. In contrast to traditional Computation Tree Logic CTL, the path quantifiers are not bound to specific linear modalities, resulting in a more expressive language. We present a sound and complete hypersequent calculus for CTL*. The proof system is cyclic in the sense that proofs are finite derivation trees with back-edges. A syntactic success condition on non-axiomatic leaves guarantees soundness. Completeness is established by relating cyclic proofs to a natural ill-founded sequent calculus for the logic.

Cite as

Bahareh Afshari, Graham E. Leigh, and Guillermo Menéndez Turata. A Cyclic Proof System for Full Computation Tree Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{afshari_et_al:LIPIcs.CSL.2023.5,
  author =	{Afshari, Bahareh and Leigh, Graham E. and Men\'{e}ndez Turata, Guillermo},
  title =	{{A Cyclic Proof System for Full Computation Tree Logic}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.5},
  URN =		{urn:nbn:de:0030-drops-174664},
  doi =		{10.4230/LIPIcs.CSL.2023.5},
  annote =	{Keywords: Full computation tree logic, Hypersequent calculus, Cyclic proofs}
}

Document

DOI: 10.4230/LIPIcs.TLCA.2015.1

Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars

Authors: Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract

Recently a new connection between proof theory and formal language theory was introduced. It was shown that the operation of cut elimination for proofs in first-order predicate logic involving Pi_1-cuts corresponds to computing the language of a particular class of regular tree grammars. The present paper expands this connection to the level of Pi_2-cuts. Given a proof pi of a Sigma_1 formula with cuts only on Pi_2 formulæ, we show there is associated to pi a natural context-free tree grammar whose language is finite and yields a Herbrand disjunction for pi.

Cite as

Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh. Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{afshari_et_al:LIPIcs.TLCA.2015.1,
  author =	{Afshari, Bahareh and Hetzl, Stefan and Leigh, Graham E.},
  title =	{{Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{1--16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.1},
  URN =		{urn:nbn:de:0030-drops-51516},
  doi =		{10.4230/LIPIcs.TLCA.2015.1},
  annote =	{Keywords: Classical logic, Context-free grammars, Cut elimination, First-order logic, Herbrand's theorem, Proof theory}
}

Document

DOI: 10.4230/LIPIcs.CSL.2013.30

On closure ordinals for the modal mu-calculus

Authors: Bahareh Afshari and Graham E. Leigh

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract

The closure ordinal of a formula of modal mu-calculus mu X phi is the least ordinal kappa, if it exists, such that the denotation of the formula and the kappa-th iteration of the monotone operator induced by phi coincide across all transition systems (finite and infinite). It is known that for every alpha < omega^2 there is a formula phi of modal logic such that mu X phi has closure ordinal alpha (Czarnecki 2010). We prove that the closure ordinals arising from the alternation-free fragment of modal mu-calculus (the syntactic class capturing Sigma_2 \cap Pi_2) are bounded by omega^2. In this logic satisfaction can be characterised in terms of the existence of tableaux, trees generated by systematically breaking down formulae into their constituents according to the semantics of the calculus. To obtain optimal upper bounds we utilise the connection between closure ordinals of formulae and embedded order-types of the corresponding tableaux.

Cite as

Bahareh Afshari and Graham E. Leigh. On closure ordinals for the modal mu-calculus. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 30-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{afshari_et_al:LIPIcs.CSL.2013.30,
  author =	{Afshari, Bahareh and Leigh, Graham E.},
  title =	{{On closure ordinals for the modal mu-calculus}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{30--44},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.30},
  URN =		{urn:nbn:de:0030-drops-41889},
  doi =		{10.4230/LIPIcs.CSL.2013.30},
  annote =	{Keywords: Closure ordinals, Modal mu-calculus, Tableaux}
}

Search Results

Documents authored by Leigh, Graham E.

A Cyclic Proof System for Full Computation Tree Logic

Abstract

Cite as

Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars

Abstract

Cite as

On closure ordinals for the modal mu-calculus

Abstract

Cite as

Thanks for your feedback!

Could not send message