Author name cluster

Graham E. Leigh

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

CSL Conference 2023 Conference Paper

A Cyclic Proof System for Full Computation Tree Logic

Bahareh Afshari
Graham E. Leigh
Guillermo Menéndez Turata

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.

Details

FLAP Journal 2016 Journal Article

Reflecting on Truth.

Graham E. Leigh

What is implicit in the acceptance of the Tarskian truth biconditionals? In this article we expand and generalise results by Horsten and Leigh [14] to characterise the proof- and truth-theoretic content of iterated reﬂection over disquotational theories of truth. In particular, we conﬁrm the conjecture that, modulo reﬂection, all there is to typed and Kripke–Feferman truth is captured by simple and natural collections of truth (and in the latter case falsity) bicon- ditionals.

PDF Details

CSL Conference 2013 Conference Paper

On closure ordinals for the modal mu-calculus

Bahareh Afshari
Graham E. Leigh

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.

Details