HLK ● ProofTool
TU Vienna ► logic.at ► Theory and Logic Group (E185-2)

CERESω

Summary

$\CERESomega$ is an extension of CERES to higher order logic. Please be sure to read the material on CERES before continuing. On this page, we will focus on the description of the differences between $\CERES$ and $\CERESomega$. For details on $\CERES$, please see Hetzl, Leitsch, Weller and Woltzenlogel Paleo 2009, Weller 2010 and Hetzl, Leitsch and Weller 2011.

The $\CERESomega$ system included in the generic architecture for proofs framework contains the implementation of the method, which at the moment provides the sequent calculus $\LKskco$ and the characteristic sequent set computation for higher order proofs.

The method

The $\CERESomega$ method proceeds analogously to the CERES method for first-order logic. As input, the method takes a proof in a higher-order version of $\LK$, which is the usual $\LK$ with additional higher-order quantifier rules

\begin{displaymath} \infer[\foralllnt]{\forall\HT{R}, \Gamma \seq \Delta}{ \HT{R... ...\seq \Delta, \forall \HT{R}} {\Gamma \seq \Delta,\HT{R}\HT{X}} \end{displaymath}

for all higher-order quantifiers, where $\HT{T}$ and $\HT{R}$ are terms, and $\HT{X}$ is a variable, and all are of appropriate types. $\beta$-reduction is implicit, and all formulas in a proof are in $\beta$-normal form.

Such a proof is translated into a proof in the $\LKskco$ calculus (which is the step corresponding to the Skolemization transformation in first-order CERES). This calculus operates on labelled sequents written $\ls{\HT{F}_1}{\ell_1},\ldots,\ls{\HT{F}_n}{\ell_n} \seq \ls{\HT{F}_{n+1}}{\ell_{n+1}},\ldots,\ls{\HT{F}_m}{\ell_m}$, which are usual higher-order sequents where to every formula in the sequent, a multiset of terms called a label is associated. $\LKskco$ is essentially $\LK$, where the eigenvariable condition is removed and instead, Skolem terms are introduced. The arguments of the Skolem functions are tracked by the labels. This yields the quantifier rules

\begin{displaymath} \infer[\forallsklnt]{\ls{\forall_\alpha\HT{F}}{\ell}, \Gamma... ... \seq \Delta, \ls{\HT{F}(\SF{f}\HT{S}_1\ldots\HT{S}_n)}{\ell}} \end{displaymath}

where $\ell=\HT{S}_1,\ldots,\HT{S}_n$ and $\SF{f}$ is a Skolem function.

From such an $\LKskco$-proof $\pi$, a set of labelled sequents $\CL(\pi)$, the characteristic sequent set, can be extracted (which corresponds to the characteristic clause set of first-order CERES). Finally, the $\Ral$ calculus

\begin{displaymath} \infer[\notT]{\ls{\HT{A}}{\ell},\Gamma\seq\Delta}{\Gamma\seq... ...ta,\ls{\HT{A}}{\ell}}{\ls{\neg \HT{A}}{\ell},\Gamma\seq\Delta} \end{displaymath}


\begin{displaymath} \infer[\orT]{\Gamma\seq\Delta,\ls{\HT{A}}{\ell}, \ls{\HT{B}}... ...Gamma\seq\Delta}{\ls{\HT{A}\vee\HT{B}}{\ell},\Gamma\seq\Delta} \end{displaymath}


\begin{displaymath} \infer[\allT]{\Gamma\seq\Delta, \ls{\HT{A}\HT{X}}{\ell,\HT{X... ...eq\Delta} \qquad \infer[\Sub]{S\subst{\HT{X}\goesto\HT{T}}}{S} \end{displaymath}


\begin{displaymath} \infer[\Cut]{\Gamma,\Pi\seq\Delta,\Lambda}{ \Gamma\seq\Delta... ...HT{A}}{\ell_{n+1}},\ldots,\ls{\HT{A}}{\ell_m},\Pi\seq\Lambda } \end{displaymath}

is used to refute the characteristic sequent set. From such a refutation, a cut-free $\LK$ proof of the original end-sequent can be computed.