Disjunctive logic programs, answer sets, and the cut rule

1.1 Disjunctive logic programs, fixed points, and negation

As noted in [19], the field of disjunctive logic programming had its beginnings in 1982, but the first major semantics for disjunctive logic programs were proposed in 1990, in [17], which offered, in particular, a natural generalisation of the fixed point semantics for definite logic programs given in [27]. The key feature of that generalised semantics is that disjunctions of atoms are generated using a bottom-up approach applied to sets of rules, assumed to have (possibly empty) conjunctions of atoms as bodies and nonempty disjunctions of atoms as heads. The model-theoretic interpretation is easy and flexible, as the absence of negation in the rules allows one to interpret disjunction either constructively or not, and also to choose for intended interpretations either all structures, all standard (Herbrand) structures, or all minimal standard structures.

It has been observed, in [21] in particular, that the generation process at work in [17] is a form of application of the hyper-resolution rule, that involves a finite but arbitrary number of clauses, as opposed to classical resolution that uses precisely two clauses as premises. Resolution, like modus ponens, is a form of the cut rule. We will refer to the cut rule to motivate and describe a generalisation to the immediate consequence operator associated with the fixed point semantics studied in [17]. The target will be the more general class of disjunctive logic programs with possibly empty heads, and more crucially, with possible occurrences of negation in the bodies and in the heads of the rules. Before we clarify what we actually mean by “occurrences of negation,” let us recall that the field of logic programming has first focused on logic programs without negation, then logic programs with nonclassical negation in the bodies of the rules, and then logic programs with nonclassical negation in the bodies of the rules and classical negation in the bodies and the heads of the rules; see [2] for a survey. Some researchers have also proposed to consider more than two forms of negation [1].

Similarly to the situation with normal programs (sets of rules with no disjunction in the heads), different views on nonclassical negation have given rise to a large number of alternative semantics. “Failure to derive” is a notion that can be applied to sets of rules with no occurrence of (any form of) negation, and [17] already establishes a relationship between their fixed-point semantics and the generalised closed world assumption. When nonclassical negation is allowed to occur in the bodies of the rules, many possible interpretations become possible. But the various interpretations of nonclassical negation do not exhaust all issues raised by the presence of negation in logic programs: in [12], an argument is made that it is often desirable to be able to work with even more powerful disjunctive programs, in which classical negation can be used, and the answer set semantics is proposed as a natural alternative semantics able to deal with both classical and nonclassical negation. See [3, 7, 23] for other approaches and complexity results on disjunctive logic programs where both nonclassical and classical negation coexist.

Let us focus on classical negation first. What happens to the fixed point semantics in [17] when classical negation enters the stage? A technique to reduce programs with classical negation to programs without is proposed in both [12] and in [24] and discussed in [18]^{Footnote 1}; essentially, for every predicate symbol \(\wp \), a new predicate symbol \(\wp ^{\lnot }\) is introduced, that allows one to get rid of \(\lnot \) by replacing the occurrences of \(\lnot \wp \) with \(\wp ^{\lnot }\), and (taking \(\wp \) to be nullary not to clutter the discussion) an integrity constraint \(\leftarrow \wp \wedge \wp ^{\lnot }\) is added to express mutual exclusivity between \(\wp \) and \(\wp ^{\lnot }\). The immediate consequence operator in [17], slightly generalised to accept rules with an empty head, can then be applied. For instance, the rules \(p\leftarrow \) and \(\lnot p\vee \lnot q\leftarrow \) are transformed into \(p\leftarrow \) and \(p^{\lnot }\vee q^{\lnot }\leftarrow \), which complemented with \(\leftarrow p\wedge p^{\lnot }\), allows the immediate consequence operator in [17] generalised to accept rules with an empty head to generate \(q^{\lnot }\); and if one added the rule \(\lnot q\leftarrow q^{\lnot }\), then one would eventually generate \(\lnot q\), as required from a complete proof procedure. This solution is not fully satisfactory though, as one has obtained a complete proof procedure for an extension of the original set of rules, not for the set of rules itself. Our immediate consequence operator will be strongly related to the one in [17], but will deal gracefully with classical negation, without enriching the original language.

Now let us focus on nonclassical negation. In close relationship to stable autoepistemic expansions ( [14, 20]), [26] lets the language of disjunctive logic programs include a modal operator \({\mathcal {B}}\) that is used to capture nonclassical negation in one of two ways: \({{\textit{not}\ }}\wp \) is expressed as either \({\mathcal {B}}\lnot \wp \) or \(\lnot {\mathcal {B}}\wp \), conveying that \(\lnot \wp \) is believed or that \(\wp \) is not believed, respectively. So classical negation is used in combination with \({\mathcal {B}}\) in one of the two proposed translations of not. As for classical negation in the original program, it gives rise in [26] to a third form of negation, denoted \(\mathord \sim \) and referred to as “strong” negation. Based on a relation of minimal model entailment, [5, 26] define a notion of static expansion that yields a fixed-point semantics for disjunctive logic programs; the associated notion of logical consequence is not standard as it requires selecting, amongst all possible interpretations, those that happen to be minimal according to an underlying notion of closed-world assumption. In this paper, we will show that we can further exploit the power of modal operators and work in a classical framework, in which classical negation is the only form of negation, a theme which has been developed in depth in [15]. Disjunctive logic programs will be modal disjunctive sets of rules, and the least fixed point of such a set of rules \({\mathcal {F}}\) will consist precisely of the disjunctions that are logical consequences of \({\mathcal {F}}\). In contrast to [26] in which the heads and bodies of rules are disjunctions and conjunctions of both formulas with no occurrence of \({\mathcal {B}}\) and formulas with occurrences of \({\mathcal {B}}\), our “building blocks” will be formulas of the form \(\Box \varphi \) or \(\Diamond \Box \varphi \) where \(\varphi \) is a literal. More specifically, given an atom \(\wp \), we will map \(\wp \) to \(\Box \wp \), \(\lnot \wp \) to \(\Box \lnot \wp \), \({{\textit{not}\ }}\wp \) to \(\Diamond \Box \lnot \wp \) and \({{\textit{not}\ }}\lnot \wp \) to \(\Diamond \Box \wp \). This mapping is studied in depth in the context of nondisjunctive logic programs in [16]. One of the key properties of the proposed syntax of rules is that disjunction is constructive. In [26], it is claimed that “as pointed out by several researchers, the form of negation proposed by Gelfond and Lifschitz does not represent real classical negation \(\lnot F\) but rather its weaker form, denoted here by \(\mathord \sim F\), which does not require the law of excluded middle \(F\vee \mathord \sim F\).” This paper adopts a different view, namely, that only classical negation is necessary, and that there are other ways to circumvent excluded middle than to introduce a weaker form of negation; rather than expressing that either F or \(\lnot F\) holds, one can express that either F or \(\lnot F\) has been derived, that is, \(\Box F\vee \Box \lnot F\), in accordance with Gödel’s interpretation of intuitionistic logic in S4. Our representation of not allows disjunction to behave constructively with respect to both \(\lnot \) and not, as \(\Box p\vee \Diamond \Box \lnot p\) will not be valid. In contrast, \(\Box p\vee \Diamond \lnot p\) would be valid, so \(\Diamond \Box \) cannot be replaced by \(\Diamond \); our results will provide evidence that for our purposes, \(\Diamond \Box \) is the right choice. There are many examples of frameworks where the “building blocks” are of the form \(\Box \varphi \) and \(\Diamond \varphi \), in particular within the setting of autoepistemic logic (e.g., [10]), but not only (e.g., [22]).

1.2 Answer sets and program transformation

Let us describe the answer set semantics with an example. Consider the following set of rules, \({\mathcal {R}}\).

It has \(X=\{\lnot p_1,\,p_2,\,p_4\}\) as an answer set. Indeed, let us replace in (the bodies of the rules in) \({\mathcal {R}}\) all formulas of the form \({{\textit{not}\ }}\psi \) by \( true \) if \(\psi \notin X\), by \( false \) otherwise, and simplify. This is the Gelfond-Lifschitz transformation [11]. It results in the following set of rules, \({\mathcal {R}}'\):

For all atoms \(\alpha \), replace in \({\mathcal {R}}'\) all occurrences of \(\lnot \alpha \) by a new atom \(\alpha ^\star \), resulting in a new set of rules, \({\mathcal {R}}''\):

The logical consequences of \({\mathcal {R}}''\) is \(\{p_1^\star ,\,p_2,\,p_4\}\), and that set consists precisely of the members of X where all negated atoms of the form \(\lnot \alpha \) have been replaced by \(\alpha ^\star \), completing the verification that X is an answer set for \({\mathcal {R}}\).

The answer set semantics imposes a condition that in our framework, translates into complementing the (modal version of the) logic program with a set of formulas of the form \(\Diamond \Box \varphi \). More precisely: if \(\Diamond \Box \varphi \) occurs in the (modal version of the) logic program, then that program should be complemented with \(\Diamond \Box \varphi \) provided that the resulting set of formulas does not logically imply \(\Box \lnot \varphi \) (which will logically imply \(\Box \Diamond \lnot \varphi \), hence be logically inconsistent with \(\Diamond \Box \varphi \)). One can think of this condition as: any possible hypothesis \(\psi \)—formula of form \(\Diamond \Box \varphi \) that occurs in the body of some rule—should be made, unless the resulting theory (the modal logic program complemented with the set of selected hypotheses) refutes \(\psi \).^{Footnote 2} If we were dealing with normal programs, then no other machinery would be needed to capture the answer set semantics. But as we are dealing with logic programs whose heads are disjunctions of (one or more) literals, it is necessary to introduce one more component. Indeed, the cut rule will not be applied to \({\mathcal {F}}\), but to a closure of \({\mathcal {F}}\) under an operation that creates more rules, while still preserving logical validity (the created rules will be logical consequences of those from which they originate). What is required is a form of program extension, a particular case of program transformation. Program transformation is a technique that has been widely used in logic programming in general, and for the particular purpose of defining semantics of disjunctive programs, for example in [4]. Essentially, the transformation we shall use will, from a rule of the form^{Footnote 3}

produce rules of the following form.

In a different syntactic setting, this operation was studied in [6] to transform disjunctive programs into a normal program. In our framework, the original set of rules will not be replaced by, but complemented with, formulas obtained by left-shift. The answer set semantics lets literals assumed not to hold play a role in activating a rule by having them preceded with not in the body of the rule. Translated into our setting, the set of literals preceded with not in the bodies of some rules makes up a sufficient pool of hypotheses to cast the answer set semantics, provided the focus is on normal programs. But when dealing with disjunctive logic programs, this pool of literals is not sufficient, and the operation above, that left-shifts some formulas and turns their negations into hypotheses, makes it possible to usefully expand it as needed, no more, no less, and capture exactly the classical notion of an answer for a disjunctive logic program, as defined for instance in [10]. Interestingly, this operator is not only necessary in relation to the answer set semantics, but also for what we referred to above as the “base semantics,”, that is, essentially, the fixed point semantics in [17] generalised to disjunctive logic programs with classical negation.

There are alternative approaches to cast the answer set semantics in a logical framework where the rules of a logic program are modified or complemented with other formulas. The framework can be classical; see for instance [13], where “loop formulas” are added, in a setting restricted to logic programs without classical negation, and more importantly, limited to finite sets of finite rules—two conditions that we do not impose. The framework can be nonclassical; see for instance [25], in a setting that sits between intuitionistic logic and classical logic. There is a vast literature that examines how to compute answer sets; see [9] for a good example of work along those lines. Our study sheds no light on how to compute answer sets. Our framework is not classical in the sense that classical logical inferences would make it possible to derive, from a fixed theory, all answer sets and nothing but answer sets. Rather, its key features are the following.

• It allows one to formalise a very general class of logic programs, with mechanical translations into the chosen logical language.

• It characterises semantics of interest in the form of some formulas being logical consequences of some theory T, possibly together with conditions imposing that certain formulas be or be not logical consequences of T.

• It is a unifying framework in that the characterisations all rely on a fixed set of underlying notions and a fixed classical notion of logical consequence (a claim that is partially supported by the work described in this paper, but more strongly so thanks to the additional work presented in other papers).

1.3 Plan of the paper

We proceed as follows. In Sect. 2, we motivate the notions to be introduced in the rest of the paper. In Sect. 3, we fix the logical background, and in particular, define the modal language from which the bodies and heads of a disjunctive logic program will be made up, together with its semantics. In Sect. 4, we formalise the left shift operation and establish the relationship between this framework and the answer set semantics; the rest of the paper can then be applied to the answer set semantics as a particular case. In Sect. 5, we introduce an intermediate proof system, in the spirit of tableau proofs, and establish its completeness with respect to the class of disjunctive logic programs under consideration. In Sect. 6, we let the cut rule be a counterpart to the immediate consequence operator described in [17]; we then establish the completeness of the system of proof based on applications of this rule. Essentially, we convert a tableau proof into a proof by cuts, a technique which is interesting in its own right.

2.1 Objective

Consider the very simple sets of rules whose left hand sides are empty or positive propositional formulas (built from atoms using conjunction and disjunction) and whose right hand sides are atoms.^{Footnote 4} Here is an example of such a set of rules \({\mathcal {P}}\):

One can describe the set of literals \([{\mathcal {P}}]\) that are logical consequences of this set of implications, namely, \(\{p_1,p_2,p_3,p_5,p_8,p_{10}\}\), as the \(\subseteq \)-minimal fixed point of \({\mathcal {P}}\). One can also describe it as the result of

• first collecting the facts—the right hand sides of the rules with empty left hand sides—and

• then firing the rules that can be activated because the atoms generated so far validate their left hand sides, and collecting their right hand sides.

That yields successively \([{\mathcal {P}}]_0=\{p_1,p_2\}\), \([{\mathcal {P}}]_1=\{p_1,p_2,p_3\}\), \([{\mathcal {P}}]_2=\{p_1,p_2,p_3,p_5\}\), and finally, \([{\mathcal {P}}]_3=[{\mathcal {P}}]\). In a first-order setting where interpretations are standard and might have infinite domains and where rules accommodate existential and universal quantifiers, the iterative process of generating atoms could be transfinite, but there would still be a unique \(\subseteq \)-minimal fixed point \([{\mathcal {P}}]\), equal to \([{\mathcal {P}}]_{\alpha \in \mathrm {Ord}}\) where \(\mathrm {Ord}\) denotes the class of ordinals; as \(\mathrm {Ord}\) is a proper class, \([{\mathcal {P}}]_\alpha \) is guaranteed to be equal to \(\bigcup _{\beta <\alpha }[{\mathcal {P}}]_\beta \) for some least ordinal \(\alpha \), marking the point at which the whole of \([{\mathcal {P}}]\) has been generated. What are the key features of this generation process?

1. (A)

   Rules are read from left to right, they operate from the left hand side to the right hand side; the contrapositives of the rules can be ignored.

2. (B)

   At any stage, rules can be considered individually, independently of any others, to determine what to generate at the next stage.

3. (C)

   At any stage, what is generated involves a rule whose left hand side is “validated” with what has been previously generated.

The theme of this paper is that properties (A)–(C) can be preserved for rules that are more interesting and general, and more particularly, for rules with disjunctions on the right hand side; moreover, an adapted form of the cut rule can operate on rules in a way that satisfies properties (A)–(C).

The most elegant presentation of the cut rule is in the sequent calculus, and takes the form

to express that

is a logical consequence of

and

We will go through intermediate sets of rules and intermediate adaptations of the cut rule till we reach the final form of the cut rule that can be satisfactorily applied to the sets of rules of the kind that we want to eventually be able to work with. Let us first adapt the cut rule so that it can deal with sets of rules of the form described above, in a way that satisfies properties (A)–(C) above: we let it take the form

where \(k\in \mathbb {N}\), \(\xi _0\), ..., \(\xi _k\), \(\psi \) are atoms, \(\varphi \) is a positive propositional formula with at least one occurrence of each of \(\xi _0\), ..., \(\xi _k\), and \(\varphi [\xi _0/ true ,\dots ,\xi _k/ true ]\), that is, the result of making all occurrences of \(\xi _0\), ..., \(\xi _k\) in \(\varphi \) true, is logically valid. This is a big modification of (\(\star \)), and in some way also a big simplification, more similar to a generalised modus ponens than to a full cut, but further adaptations will bring us closer to (\(\star \)) as we consider sets of rules with disjunction on the right hand side. As an example of an application of (\(\diamond \)) for the set of rules \({\mathcal {P}}\) defined above, \(p_{10}\) is added to \([{\mathcal {P}}]\) by the following application of (\(\diamond \)):

Let us emphasise the key differences between (\(\star \)) and (\(\diamond \)), that will be applicable to all further adaptations of the cut rule.

• In (\(\star )\), the cut rule has two antecedents. In (\(\diamond \)), at least two sequents, but possibly more, make up the antecedents.

• In (\(\star )\), the antecedents of the cut rule are arbitrary sequents. In (\(\diamond \)), one antecedent of the cut rule is an arbitrary sequent, but all other antecedents are sequents with an empty left hand side.

• In (\(\star \)), the formula to which the cut is applied, namely \(\xi \), is one of a number of formulas on the left hand side of a sequent that are implicitly conjuncted. In (\(\diamond \)), the formulas \(\xi _0\), ..., \(\xi _k\) to which the cut is simultaneously applied occur in a formula \(\varphi \) that is not necessarily the conjunction of \(\xi _0\), ..., \(\xi _k\), but that is logically implied by that conjunction.

• In (\(\star \)), the consequent is an arbitrary sequent. In (\(\diamond \)), it is a sequent with an empty left hand side.

2.2 Negation

To see whether negation is problematic, let \({\mathcal {P}}\) now denote the extension of the set of rules defined above with the following rules.

One might think that the contrapositive of the first extra rule should let \(p_{11}\) join \([{\mathcal {P}}]\), breaking down property (A) above, and the last two extra rules taken together should let \(p_{13}\) join \([{\mathcal {P}}]\), breaking down properties (B) and (C). But following standard practice in logic programming, we work in a paradigm where disjunction is constructive. For example, given literals \(\varphi _1\), \(\varphi _2\), \(\varphi _3\) and \(\varphi \), the intended meaning of the rule \(\varphi _1\wedge (\varphi _2\vee \varphi _3)\rightarrow \varphi \) is, in that paradigm: if \(\varphi _1\) has been generated, and if at least one of \(\varphi _2\) and \(\varphi _3\) has been generated, then \(\varphi \) can be generated. A representation of our set of rules more faithful to that intended meaning uses the modal operator \(\Box \) to capture the notion “has been generated” or “has been proved.” And in accordance with the expected meaning of \(\Box \), we will work in a logical setting where for all atoms \(\varphi \), \(\Box \varphi \wedge \Box \lnot \varphi \) is inconsistent, while \(\Box \varphi \vee \Box \lnot \varphi \) is satisfiable but not valid. Call claim any formula of the form \(\Box \varphi \) where \(\varphi \) is a literal, and claiming condition^{Footnote 5} any formula obtained from the set of claims by arbitrary application of conjunction and disjunction. So we now consider sets of rules whose left hand sides are claiming conditions and whose right hand sides are claims.

Following on from our example, let \({\mathcal {F}}\) denote:^{Footnote 6}

We also define \([{\mathcal {F}}]\) as the set of claims that are logical consequences of \({\mathcal {F}}\). The contrapositive of the implication \(\Box \lnot p_{11}\rightarrow \Box \lnot p_3\) is a formula that is logically equivalent to \(\Diamond p_3\rightarrow \Diamond p_{11}\), which allows one to generate \(\Diamond p_{11}\) but not the stronger \(\Box p_{11}\), and as \(\Box p_{12}\vee \Box \lnot p_{12}\) is not valid, \(\Box p_{13}\) cannot be generated either. Hence

Though it uses classical negation and no other form of negation, this modal representation and associated interpretation of a set of rules is suitable to model negation as failure and the main semantics of logic programs. It is easy to see that properties (A)–(C) above are preserved for the kind of rules now under consideration, thanks to the form of the cut rule that has been described as (\(\diamond \)) with the only difference that \(\xi _0\), ..., \(\xi _k\), \(\psi \) are claims rather than atoms, and \(\varphi \) is a claiming condition rather than a positive propositional formula.

2.3 Disjunction

Let us now allow disjunction on the right hand side of a rule. Call alternative any formula of the form \(\varphi _1\vee \cdots \vee \varphi _n\) where \(n\in \mathbb {N}\) and \(\varphi _1\), ..., \(\varphi _n\) are pairwise distinct claims, with no a priori reference to any particular rule (when \(n=0\), the alternative is empty). So we now consider sets of rules whose left hand sides are claiming conditions and whose right hand sides are alternatives. Let us extend our running example so that \({\mathcal {F}}\) now denotes the set of rules above complemented with the following rules.

And now, we let \([{\mathcal {F}}]\) denote the set of alternatives that are logical consequences of \({\mathcal {F}}\). Clearly, we then have to add \(\Box p_{15}\), \(\Box \lnot p_{16}\), \(\Box p_{17}\) and \(\Box p_{20}\) to \([{\mathcal {F}}]\). But the very idea of rules that read from left to right and fire individually seems to break down. Consider first the claims \(\Box p_{15}\) and \(\Box p_{17}\). Each of them is inferred from two generated alternatives (\(\Box \lnot p_3\vee \Box p_{15}\) and \(\Box p_3\), and \(\Box p_{16}\vee \Box p_{17}\) and \(\Box \lnot p_{16}\), respectively), breaking down property (C) above. This is still easily fixed by closing \({\mathcal {F}}\) under a left shift operation, that moves claims from right to left as exemplified below, in a way that will preserve the logical validity of the original set of rules and capture well the reasoning behind the inference of \(\Box p_{15}\) from \(\Box \lnot p_3\vee \Box p_{15}\) and \(\Box p_3\), and the inference of \(\Box p_{17}\) from \(\Box p_{16}\vee \Box p_{17}\), \(\Box \lnot p_{16}\) and \(\Box p_{10}\):

\(\Box p_3\ \rightarrow \ \Box p_{15}\)            \(\Box p_{10}\wedge \Box \lnot p_{16} \ \rightarrow \ \Box p_{17}\)

When we define more formally the syntax of a rule, we will, for good reasons, take disjunction and conjunction as operators on sets. This is why we assumed that all claims that occur in an alternative are pairwise distinct. For an illustration, the fact that \(\rightarrow \Box p\vee \Box p\) is not an admissible rule implies that \(\Box \lnot p\rightarrow \Box p\) is not admissible either (it would have to be obtained from the latter by left shift); that is good, as would \(\Box \lnot p\rightarrow \Box p\) be admissible, it could be demanded that it lets one derive \(\Box p\), but \(\Box p\) cannot be derived from \(\Box \lnot p\rightarrow \Box p\) in a way that satisfies properties (A)–(C) above. Also note that a left shift can move the whole right hand side of a rule to the left. That will allow one to deal with inconsistent sets of rules and reduce any particular contradiction, involving two claims of the form \(\Box p\) and \(\Box \lnot p\), to the “generic” contradiction that emerges when the empty alternative (disjunction without disjunct) is derived, as is the case for instance for a set of rules that contains both \(\rightarrow \Box p\) and \(\rightarrow \Box \lnot p\), with \(\Box p\rightarrow \) produced from the latter by left shift.

Now consider the claim \(\Box p_{20}\). Here it seems that in order to generate \(\Box p_{20}\), it is necessary to consider, together with \(\Box p_{18}\vee \Box p_{19}\), both rules \(\Box p_{18}\rightarrow \Box p_{20}\) and \(\Box p_{19}\rightarrow \Box p_{20}\), breaking down property (B) above. This is the point where the cut rule has to be generalised from (\(\diamond \)) to a form that brings it closer to (\(\star \)): we now let it take the form

where

• \(k,n_0,\dotsc ,n_k,n,m\in \mathbb {N}\), \(\xi _0^0\), ..., \(\xi _0^{n_0}\) are pairwise distinct claims, ..., \(\xi _k^0\), ..., \(\xi _k^{n_k}\) are pairwise distinct claims, \(\psi _0\), ..., \(\psi _n\) are pairwise distinct claims,

• \(\varphi \) is a claiming condition with at least one occurrence of each of \(\xi _0^{n_0}\), ..., \(\xi _k^{n_k}\),

• \(\varphi [\xi _0^{n_0}/ true ,\dots ,\xi _k^{n_k}/ true ]\) is logically valid, and

• \(\xi _1,\dots ,\xi _m\) are the pairwise distinct members of \(\{\xi _i^j\mid i\le k,\,j<n_i\}\) that do not belong to \(\{\psi _0,\dotsc ,\psi _n\}\) .

For instance, we can add \(\Box p_{20}\) to \([{\mathcal {F}}]\) thanks to two applications of (\(\dagger \)):

One can see that the logically strongest members of \([{\mathcal {F}}]\) can be obtained by successive applications of (\(\dagger \)) on the closure of \({\mathcal {F}}\) under left shift, validating properties (A)–(C) above.

One might object that the order of the claims on the right hand side of a sequent has to be taken into account, and that it is necessary to add a rule that permutes the various elements of a sequence so that the claims to which the cut is applied can always be last on the right hand side of the corresponding sequents. But this will not be necessary again because disjunction will be treated as an operator over a set: the right hand side of a sequent in (\(\dagger \)) is implicitly disjuncted as a set, and is therefore to be conceived of as some arbitrary enumeration of that set, the order of the enumeration being irrelevant. One could therefore write the right hand side of a sequent either as \(\{\xi _1,\dotsc ,\xi _n\}\) or as \(\bigvee \{\xi _1,\dotsc ,\xi _n\}\) rather than as \(\xi _1,\dotsc ,\xi _n\), depending on whether which of making the disjunction implicit or explicit would be preferred.

2.4 Answer sets

Can we consider positive formulas over a set of formulas that is not constrained to containing claims only? As we work in a constructive paradigm, and as for all literals \(\varphi \), \(\Box \varphi \vee \Diamond \lnot \varphi \) will be valid, we have to keep formulas of the form \(\Diamond \varphi \) out of both sides of the rules. But we will work in a logical framework where for all literals \(\varphi \), \(\Diamond \Box \varphi \) is a logical consequence of \(\Box \varphi \), is consistent with \(\Diamond \Box \lnot \varphi \) and is inconsistent with \(\Box \lnot \varphi \), and where \(\Diamond \Box \varphi \vee \Diamond \Box \lnot \varphi \) is not valid. Call hypothesis any formula of the form \(\Diamond \Box \varphi \) where \(\varphi \) is a literal (so a hypothesis is any formula of the form \(\Diamond \varphi \) where \(\varphi \) is a claim). We now motivate why hypotheses are interesting and why it is worth allowing them to occur on the left hand side of the rules, motivated by relationships to the answer set semantics.

The usual presentation of the answer set semantics uses two kinds of negation: classical \(\lnot \) and nonclassical not. The former can only be applied to atoms, and the latter to atoms or classically negated atoms; moreover, not can only occur on the left hand side of a rule, and the right hand side of a rule can be either a literal or a disjunction. Such sets of rules are referred to as extended-disjunctive programs, and as extended-normal in case disjunction does not occur on the right hand side of any rule. One can transform an extended-disjunctive program \({\mathcal {R}}\) into a set of rules \({\mathcal {R}}^\star \) that uses modalities but not not, proceeding as follows.

• Precede all occurrences of literals preceded with neither not nor \(\lnot \) with \(\Box \).

• Replace every occurrence of not which is not followed by \(\lnot \) with \(\Diamond \Box \lnot \).

• Replace every occurrence of \({{\textit{not}\ }}\lnot \) with \(\Diamond \Box \).

For instance, this technique transforms the following extended-normal program \({\mathcal {R}}\), already met in Sect. 1.2,

into the following set of rules \({\mathcal {R}}^\star \).

Call condition, with no a priori reference to any particular rule, any formula obtained from the set of claims and hypotheses by arbitrary application of conjunction and disjunction. We have now reached the final form of the rules we want to be able to work with: they have conditions as left hand sides, and alternatives as right hand sides—let us refer to them as conditional alternatives.

Given an extended-normal program \({\mathcal {R}}\), let us examine the relationship between \({\mathcal {R}}\) and the associated set of conditional alternatives \({\mathcal {R}}^\star \). It is easy to see that if \({\mathcal {R}}\) is the extended-normal program defined above, then \({\mathcal {R}}\) has a unique answer set, namely, \(\{\lnot p_1,\,p_2,\,p_4\}\),^{Footnote 7} and the set of logical consequences of \({\mathcal {R}}^\star \cup \{\Diamond \Box p_2,\,\Diamond \Box \lnot p_3\}\) is \(\{\Box \lnot p_1,\,\Box p_2,\,\Box p_4\}\). We will verify that more generally, given an extended-normal program \({\mathcal {R}}\) and a set of literals X, X is an answer set for \({\mathcal {R}}\) iff \(\{\Box \varphi \mid \varphi \in X\}\) is the set of all claims that are logical consequences of \({\mathcal {R}}^\star \cup H\) where H is a set of hypotheses with the following properties.

• \({\mathcal {R}}^\star \cup H\) is consistent;

• for all literals \(\psi \), \(\Diamond \Box \psi \) belongs to H iff \(\Diamond \Box \psi \) occurs in (the conditions of the conditional alternatives in) \({\mathcal {R}}^\star \) and \(\Box \lnot \psi \) is not a logical consequence of \({\mathcal {R}}^\star \cup H\).

Obviously, the previous relationship between \({\mathcal {R}}\) and \({\mathcal {R}}^\star \) does not generalise to extended-disjunctive programs. For instance, the extended-disjunctive program consisting of only \(\rightarrow p\vee q\) has \(\{p\}\) and \(\{q\}\) as answer sets, and neither \(\{\Box p\}\) nor \(\{\Box q\}\) is the set of claims that are logical consequences of \(\{\Box p\vee \Box q\}\) complemented with some set of hypotheses. What we need is the left-shift operation described in the previous section, adapted to let claims that move from right to left become hypotheses rather than claims, which still preserves logical validity; let us talk about hypothetical left shift to refer to this form of the left shift operator. With \(\rightarrow \Box p\vee \Box q\) as example, the hypothetical left-shift generates the three conditional alternatives that follow.

\(\Diamond \Box \lnot p\ \rightarrow \ \Box q\)      \(\Diamond \Box \lnot q\ \rightarrow \ \Box p\)      \(\Diamond \Box \lnot p\wedge \Diamond \Box \lnot q\ \rightarrow \)

The resulting set of conditional alternatives can obviously be complemented with \(\{\Diamond \Box \lnot p\}\) or \(\{\Diamond \Box \lnot q\}\) so that the set of claims that are logical consequences of the resulting theory is \(\{\Box q\}\) or \(\{\Box p\}\), respectively, which captures answer sets along the lines of what we described above in reference to an extended-normal program, but where instead of considering \({\mathcal {R}}^\star \), we consider the closure of \({\mathcal {R}}^\star \) under hypothetical left shift. Of course, the conditional alternatives introduced by hypothetical left shift might not be of any use. For instance, the extended-disjunctive program

has \(\{p,q\}\) as unique answer set, and \(\{\Box p,\Box q\}\) is the set of claims that are logical consequences of \(\{\Box p\vee \Box q,\,\Box p\rightarrow \Box q,\,\Box q\rightarrow \Box p\}\).

We can now formulate the key question that is the object of this paper in full generality.

Let \({\mathcal {F}}\) be a set of conditional alternatives and H a set of hypotheses. Let \([{\mathcal {F}},H]\) denote the set of all alternatives that are logical consequences of \({\mathcal {F}}\cup H\). Is there a form of the cut rule that can be applied to a closure of \({\mathcal {F}}\) and H and generate \([{\mathcal {F}},H]\), in such a way that properties (A)–(C) discussed at the beginning of the paper hold?

We have claimed that this question can be positively answered in case H is empty and no hypothesis occurs in \({\mathcal {F}}\), thanks to the first version of the left shift operator and the version of the cut rule given by (\(\dagger \)). We will see that there is also a positive answer in the general case. The closure of \({\mathcal {F}}\) and H will be obtained by hypothetical left shift and replacement of all occurrences of the members of H in the conditions of the conditional alternatives so obtained by \( true \). The version of the cut rule to be used is what has been described as (\(\dagger \)), except that \(\varphi \) has to be assumed to be a condition rather than a claiming condition, and the requirement that \(\varphi [\xi _0^{n_0}/ true ,\dots ,\xi _k^{n_k}/ true ]\) be logically valid has to be replaced by the requirement that

be logically valid: we set to \( true \) in the condition of the conditional alternative that is the target of the cut all hypotheses and claims built from one of the \(k+1\) literals to which the cut applies.

2.5 Dealing properly with substitution and validity

Our last form of the cut rule still leaves to be desired: eliminating the left hand side of the selected conditional alternative by turning it into a valid formula thanks to substitution of claims and hypotheses by \( t rue\) is not a mechanical, syntactic, proof-theoretic operation. But we will proceed in a way that addresses this issue satisfactorily. Recall that we intend to take disjunction and conjunction as operators on (possibly empty) sets. We have mentioned already that this has the advantage of making duplicate disjuncted claims a non-issue. Note now that there is no need to introduce a propositional constant \( t rue\) as \(\bigwedge \varnothing \) is logically valid, and that \(\bigvee \varnothing \) is logically invalid. This will be useful to avoid empty left or right hand sides in a conditional alternative, which is formally sloppy. But the key point is that we can replace the requirement that

\(\varphi [\Diamond \xi _0^{n_0}/ true ,\dots ,\Diamond \xi _k^{n_k}/ true ][\xi _0^{n_0}/ true ,\dots ,\xi _k^{n_k}/ true ]\) is logically valid

by the requirement that

\(\bigwedge \varnothing \) is the result of substituting all occurrences of \(\Diamond \xi _0^{n_0}\), ..., \(\Diamond \xi _k^{n_k}\) and all occurrences of \(\xi _0^{n_0}\), ..., \(\xi _k^{n_k}\) not preceded by \(\Diamond \) in \(\varphi \) by \(\bigwedge \varnothing \), collapsing conjunctions, collapsing disjunctions, letting \(\bigwedge \varnothing \) absorb enclosing disjunctions, and letting \(\bigvee \varnothing \) absorb enclosing conjunctions.

For an example, let \(\varphi \) be

When one replaces in \(\varphi \) the claims \(\Box p_1\), \(\Box p_2\), \(\Box p_4\) and \(\Box p_7\) by \(\bigwedge \varnothing \) and successively applies the transformations described above, one obtains

\(\bigwedge \bigl \{\bigwedge \varnothing \bigr \}\) and eventually \(\bigwedge \varnothing \). What we have described is a mechanical, syntactic, proof-theoretic way guaranteed to derive \(\bigwedge \varnothing \) from a condition in which the occurrences of some claims and hypotheses have been replaced by \(\bigwedge \varnothing \) whenever the resulting formula logically follows from the set of those claims and hypotheses.

3.1 Claims, hypotheses, and disjunctive programs

\(\mathbb {N}\) denotes the set of natural numbers and \(\mathrm {Ord}\) the class of ordinals.

Definition 3.1

A vocabulary is a countable set of nullary predicate symbols.

Notation 3.2

We denote by \({\mathcal {V}}\) a vocabulary.

Members of \({\mathcal {V}}\) are called atoms (over \({\mathcal {V}}\)). Members of \({\mathcal {V}}\) and negations of members of \({\mathcal {V}}\) are called literals (over \({\mathcal {V}}\)). Given a literal \(\varphi \), we let \(\mathord \sim \varphi \) denote \(\lnot \varphi \) if \(\varphi \) is an atom, and \(\psi \) if \(\varphi \) is of the form \(\lnot \psi \).

Definition 3.3

The set of conditions (over \({\mathcal {V}}\)) is inductively defined as the smallest set that satisfies the following conditions.

• All expressions of the form \(\Box \varphi \) with \(\varphi \) a literal over \({\mathcal {V}}\), are conditions.

• All expressions of the form \(\Diamond \Box \varphi \) with \(\varphi \) a literal over \({\mathcal {V}}\), are conditions.

• All expressions of the form \(\bigvee X\) with X a countable set of conditions over \({\mathcal {V}}\), are conditions.

• All expressions of the form \(\bigwedge X\) with X a finite set of conditions over \({\mathcal {V}}\), are conditions.

Definition 3.4

We call claim (over \({\mathcal {V}}\)) any condition over \({\mathcal {V}}\) of the form \(\Box \varphi \).

We call hypothesis (over \({\mathcal {V}}\)) any condition over \({\mathcal {V}}\) of the form \(\Diamond \Box \varphi \).

We call stance (over \({\mathcal {V}}\)) any claim or hypothesis over \({\mathcal {V}}\).

A few remarks about Definition 3.3 are in order. First, note that all conditions are in negation normal form: negation can be applied to atoms only. Second, note that disjunction and conjunction can be applied to the empty set, yielding a logically invalid and a logically valid formula, respectively. Third, note that contrary to conjunction, disjunction can be applied to an infinite set. The motivation is that it will be formally advantageous to group together all rules that have a common alternative: rather than considering a set of rules of the form \(\{\Box p_i\rightarrow \Box q\mid i\in \mathbb {N}\}\), we will prefer the single rule \(\bigvee \{\Box p_i\mid i\in \mathbb {N}\}\rightarrow \Box q\). Infinite vocabularies and infinite sets of rules are natural if one thinks of propositionalising a set of first order (modal) rules. For instance, the previous set of rules could be obtained by propositionalising the first-order rule \(\exists x\Box p(x)\rightarrow \Box q(\overline{0})\) in a setting where all intended interpretations are standard and the set of closed terms is equal to the set of numerals \(\{\overline{n}\mid n\in \mathbb {N}\}\); then one would map \(p(\overline{n})\) to \(p_n\) for all \(n\in \mathbb {N}\), \(q(\overline{0})\) to q, and obtain the former set of rules as an alternative representation. If we worked in a first-order language with standard structures as intended interpretations, that language could sometimes be kept finite thanks to function symbols when infinitely many nullary predicate symbols are needed to perform the propositionalisation. As this would bring no significant difference in the results or in their proofs, we opt for the simpler formulation of an infinite propositional language. So infinite sets of rules are natural objects of study, and disjunctions that apply to infinite sets are natural tools. Moreover, disjunctions can be assumed to operate on countably infinite sets without affecting any of the formal developments. On the other hand, many results would break down if conjunction was allowed to operate on infinite sets.

Given \(n\in \mathbb {N}\) and conditions \(\varphi _1\), ..., \(\varphi _n\), we use \(\varphi _1\vee \cdots \vee \varphi _n\) and \(\varphi _1\wedge \cdots \wedge \varphi _n\) as abbreviations for \(\bigvee \{\varphi _i \mid 1\le i\le n\}\) and \(\bigwedge \{\varphi _i \mid 1\le i\le n\}\), respectively.

Notation 3.5

We denote by \(\mathrm {Alt}({\mathcal {V}})\) the set of finite sets of literals over \({\mathcal {V}}\).

As we know from Sect. 2, we will consider rules whose right hand sides are of the form \(\bigvee \Box D\) for some member D of \(\mathrm {Alt}({\mathcal {V}})\), where \(\Box D\) is defined next.

Notation 3.6

For all \(D\in \mathrm {Alt}({\mathcal {V}})\), we let \(\mathord \sim D\) denote \(\{\mathord \sim \varphi \mid \varphi \in D\}\), \(\Box D\) denote \(\{\Box \varphi \mid \varphi \in D\}\), and \(\Diamond \Box D\) denote \(\{\Diamond \Box \varphi \mid \varphi \in D\}\).

If, as explained before, one chooses to disjunct the conditions of all rules that have a common alternative, one is then led to define the sets of rules that are our object of study as follows, using either an “implicit” representation (Definition 3.7, mapping to a unique condition the set of literals that once disjuncted, make up an alternative) or an “explicit” representation (Definition 3.9, putting the mapping in proper logical form).

Definition 3.7

We define a disjunctive program (over \({\mathcal {V}}\)) as an \(\mathrm {Alt}({\mathcal {V}})\)-family of conditions over \({\mathcal {V}}\).

Definition 3.8

We call conditional alternative (over \({\mathcal {V}}\)) any expression which is of the form \(\varphi \rightarrow \bigvee \Box D\) where \(\varphi \) is a condition over \({\mathcal {V}}\) and D a member of \(\mathrm {Alt}({\mathcal {V}})\); we call \(\varphi \) the condition of the conditional alternative and \(\bigvee \Box D\) the alternative of the conditional alternative.

Definition 3.9

Let a disjunctive program \({\mathcal {F}}=(\varphi _D)_{D\in \mathrm {Alt}({\mathcal {V}})}\) be given.

The theory associated with \({\mathcal {F}}\)is defined as the set of conditional alternatives

Notation 3.10

Given a disjunctive program \({\mathcal {F}}\), we let \(\mathrm {Th}({{\mathcal {F}}})\) denote the theory associated with \({\mathcal {F}}\).

For instance, suppose that \({\mathcal {V}}=\{p_1,\,p_2,\,p_3,\,p_4\}\). Then \(D=\{p_3,\lnot p_4\}\) is a member of \(\mathrm {Alt}({\mathcal {V}})\), and \(\varphi _D\) could be \((\Box p_1\wedge \Box p_2)\vee \Diamond \Box \lnot p_4\), in which case \({\mathcal {F}}\) would have as rule \((\Box p_1\wedge \Box p_2)\vee \Diamond \Box \lnot p_4\rightarrow \Box p_3\vee \Box \lnot p_4\). That would formalise an extended-disjunctive program having as rules \(p_1\wedge p_2\rightarrow p_3\vee \lnot p_4\) and \({{\textit{not}\ }}p_4\rightarrow p_3\vee \lnot p_4\), and no other rule with \(p_3\vee \lnot p_4\) as head. All rules with the same head are grouped together (thanks to potentially infinite disjunctions) in \({\mathcal {F}}\). In practice, for most members \(D'\) of \(\mathrm {Alt}({\mathcal {V}})\), \(\varphi _{D'}\) would be \(\bigvee \varnothing \) as \({\mathcal {F}}\) would model an extended-disjunctive program with no rule with the disjunctions of the members of \(D'\) as head (with \({\mathcal {V}}=\{p_1,\,p_2,\,p_3,\,p_4\}\), \(\mathrm {Alt}({\mathcal {V}})\)is of cardinality \(2^8\)).

Notation 3.11

Given a disjunctive program \({\mathcal {F}}=(\varphi _D)_{D\in \mathrm {Alt}({\mathcal {V}})}\), we let \(Hyp({\mathcal {F}})\) denote the set of hypotheses that occur in \(\{\varphi _D\mid D\in \mathrm {Alt}({\mathcal {V}})\}\).

3.2 Semantics

The formulas that make up the theory associated with a disjunctive program are very specific: they are implications both sides of which do not contain occurrences of a formula of the form \(\Diamond \varphi \) for some literal \(\varphi \), where no modal operator is in the scope of another modal operator except for hypotheses, etc. This implies that we do not need to develop a complete semantics for a set of formulas closed under modal and boolean operators. We opt for keeping the concepts to a minimal, and in particular, avoid to resort to Kripke frames or similar semantic objects. Instead, we restrict the notion of logical consequence we will work with to that part of the language that we strictly need. But it is perfectly possible to embed the notions defined in this section into a full fledged semantics, and this is done in [16].

Definition 3.12

Let X be a set of stances. We say that X is consistent just in case for all literals \(\varphi \), if \(\Box \varphi \in X\) then neither \(\Box \mathord \sim \varphi \) nor \(\Diamond \Box \mathord \sim \varphi \) belongs to X; otherwise we say that X is inconsistent.

Definition 3.13

A set X of stances is closed just in case it is consistent and for all literals \(\varphi \), if \(\Box \varphi \in X\) then \(\Diamond \Box \varphi \) belongs to X.

Essentially, the notion of a closed set of stances provides a convenient, syntactic definition of logical consequence between a set of stances (used as antecedent) and a stance (used as consequent) which suffices for our purposes: we can think of a stance \(\psi \) to be a logical consequence of a set X of stances iff \(\psi \) belongs to the closure of X (that is, the \(\subseteq \)-smallest set of stances which is closed and contains X).

The first part of next definition is motivated by the relationship this framework bears to the answer set semantics, as sketched in Sect. 2. The second part fulfils a different purpose: intuitively, a complete set of stances is the set of all stances that are true at a particular point in a suitable Kripke frame, which suffices to determine the truth of any condition or conditional alternative at that point, hence which suffices to define a notion of logical consequence restricted to the language of hypotheses and of the theory associated with a disjunctive program.

Definition 3.14

Let H be a set of hypotheses. A set X of stances is H-complete just in case it is consistent and for all literals \(\varphi \) with \(\Diamond \Box \varphi \in H\),

\(\Diamond \Box \varphi \in X\) iff \(\Box \mathord \sim \varphi \notin X\).

A set X of stances is complete just in case, denoting by H the set of all hypotheses, X is H-complete.

Property 3.15

A complete set of stances is closed.

Notation 3.16

We denote by \({\mathcal {S}}\) the set of all closed sets of stances (over \({\mathcal {V}}\)).

The next definition exploits the remark that precedes Definition 3.14. If we were not in a modal setting, we could think of a member of \({\mathcal {S}}\) as the atomic diagram of a standard structure that determines the truth value of any sentence in that structure. Here we can think of a member of \({\mathcal {S}}\) as the “stance diagram” of a point of a Kripke frame that determines the truth value of any condition or conditional alternative at that point.

Definition 3.17

Let a member \(\mathfrak S\) of \({\mathcal {S}}\) be given.

For \(\varphi \) a condition, we say that \(\mathfrak S\) forces \(\varphi \) and write \(\mathfrak S\mathbin {\Vdash }\varphi \) iff:

• when \(\varphi \) is a stance, \(\varphi \in \mathfrak S\);

• when \(\varphi \) is of the form \(\bigvee X\), \(\mathfrak S\) forces some member of X;

• when \(\varphi \) is of the form \(\bigwedge X\), \(\mathfrak S\) forces all members of X.

For all conditional alternatives \(\varphi \), we say that \(\mathfrak S\) forces \(\varphi \), denoted \(\mathfrak S\mathbin {\Vdash }\varphi \), iff either \(\mathfrak S\) does not force the condition of \(\varphi \) or \(\mathfrak S\) forces the alternative of \(\varphi \).

If \(\mathfrak S\) does not force a condition or a conditional alternative \(\varphi \) then we write \(\mathfrak S\mathbin {\nVdash }\varphi \).

Given a set T of conditions or conditional alternatives, we write \(\mathfrak S\mathbin {\Vdash }T\) if \(\mathfrak S\) forces all members of T, and \(\mathfrak S\mathbin {\nVdash }T\) otherwise.

Definition 3.18

Given two sets of conditions or conditional alternatives T and X, we say that X is a logical \({\mathcal {S}}\)-consequence of T, or that T logically \({\mathcal {S}}\)-implies X, and we write \(T\vDash _{\mathcal {S}}X\), just in case every member of \({\mathcal {S}}\) that forces T forces X.

If a set of conditions or conditional alternatives T does not logically \({\mathcal {S}}\)-imply a set of conditions or conditional alternatives X then we write \(T\nvDash _{\mathcal {S}}X\).

The same terminology and notation applies if one or both sets of conditions are replaced by a condition or a conditional alternative.

Definition 3.19

Given two sets of conditions or conditional alternatives \(T_1\) and \(T_2\), we say that \(T_1\) and \(T_2\) are logically \({\mathcal {S}}\)-equivalent just in case \(T_1\) logically \({\mathcal {S}}\)-implies \(T_2\) and \(T_2\) logically \({\mathcal {S}}\)-implies \(T_1\).

Definition 3.20

Let a disjunctive program \({\mathcal {F}}\) and a set H of hypotheses. We say that \({\mathcal {F}}\) is \({\mathcal {S}}\)-consistent with H just in case some member of \({\mathcal {S}}\) forces \(H\cup \mathrm {Th}({{\mathcal {F}}})\); otherwise we say that \({\mathcal {F}}\) is \({\mathcal {S}}\)-inconsistent with H.

Definition 3.21

A condition is said to be \({\mathcal {S}}\)-valid iff it is logically \({\mathcal {S}}\)-equivalent to \(\bigwedge \varnothing \).

3.3 Remarks

Let a disjunctive program \({\mathcal {F}}=(\varphi _D)_{D\in \mathrm {Alt}({\mathcal {V}})}\) be given.

First, suppose that \(\varphi _D=\bigvee \varnothing \) for all members D of \(\mathrm {Alt}({\mathcal {V}})\) that contain at least one negated atom. Also suppose that for all members D of \(\mathrm {Alt}({\mathcal {V}})\), \(\varphi _D\) contains no occurrence of a hypothesis and no occurrence of a claim of the form \(\Box \lnot p\). So \({\mathcal {F}}\) formalises a logic program whose rules are all of the form

where \(p_{i_1}\), ..., \(p_{i_n}\), \(p_{j_1}\), ..., \(p_{j_m}\) are atoms. Such are the logic programs considered in [17]. They are given a semantics, in terms of the derivation of disjunctions of the form \(p_{k_1}\vee \dots \vee p_{k_p}\), that is precisely captured by the notion of a disjunction of the form \(\Box p_{k_1}\vee \dots \vee \Box p_{k_p}\) being a logical \({\mathcal {S}}\)-consequence of \(\mathrm {Th}({{\mathcal {F}}})\). This is an immediate consequence of a very special case of Proposition 6.10, proved in Sect. 6: the proof system used to establish the validity of Proposition 6.10 corresponds to the procedure that defines the semantics presented in [17].

Second, suppose that for all members D of \(\mathrm {Alt}({\mathcal {V}})\), \(\varphi _D\) contains no occurrence of a hypothesis. So \({\mathcal {F}}\) formalises a logic program whose rules are all of the form

where \(l_{i_1}\), ..., \(l_{i_n}\), \(l_{j_1}\), ..., \(l_{j_m}\) are literals. Then the notion of a disjunction of the form \(\Box l_{k_1}\vee \dots \vee \Box l_{k_p}\) being a logical \({\mathcal {S}}\)-consequence of \(\mathrm {Th}({{\mathcal {F}}})\) also captures the semantics described in [17], but generalised to the logic programs where classical negation is accepted in the (bodies and heads) of the rules. Moreover, for all sets H of hypotheses and for all disjunctions \(\varphi \) of the form \(\Box l_{k_1}\vee \dots \vee \Box l_{k_p}\), \(\varphi \) is a logical \({\mathcal {S}}\)-consequence of \(\mathrm {Th}({{\mathcal {F}}})\) iff \(\varphi \) is a logical \({\mathcal {S}}\)-consequence of \(H\cup \mathrm {Th}({{\mathcal {F}}})\): hypotheses do not increase logical power when dealing with disjunctive programs that formalise logic program with classical negation but without not.

Third, imposing no condition on \({\mathcal {F}}\), the following holds. Let \({\mathcal {F}}'=(\varphi '_D)_{D\in \mathrm {Alt}({\mathcal {V}})}\) be the disjunctive program such that for all members D of \(\mathrm {Alt}({\mathcal {V}})\), \(\varphi '_D\) is \(\varphi _D\) with any occurence of a hypothesis of the form \(\Diamond \Box l\) being replaced by \(\Box l\). Then for all disjunctions \(\varphi \) of the form \(\Box l_{k_1}\vee \dots \vee \Box l_{k_p}\), \(\varphi \) is a logical \({\mathcal {S}}\)-consequence of \(\mathrm {Th}({{\mathcal {F}}})\) iff \(\varphi \) is a logical \({\mathcal {S}}\)-consequence of \(\mathrm {Th}({{\mathcal {F}}'})\): disjunctive programs that formalise logic programs in which not can occur in the bodies of the rules would not add logical power, if hypotheses were not introduced too as “complementary axioms”. Proposition 6.10 will embody the full generality of the proposed framework.

The next definition captures the notion of hypothetical left shift discussed in Sect. 2, here defined up to logical \({\mathcal {S}}\)-equivalence, which suffices for our purposes. A left shift completion of a disjunctive program \({\mathcal {F}}\) should be thought of as the closure of \({\mathcal {F}}\) under hypothetical left shift.

Definition 4.1

Let a disjunctive program \({\mathcal {F}}=(\varphi _D)_{D\in \mathrm {Alt}({\mathcal {V}})}\) be given. A left shift completion of \({\mathcal {F}}\)is a disjunctive program \({\mathcal {F}}'=(\varphi '_D)_{D\in \mathrm {Alt}({\mathcal {V}})}\) such that for all \(D\in \mathrm {Alt}({\mathcal {V}})\), \(\varphi '_D\) is logically \({\mathcal {S}}\)-equivalent to

For instance, suppose that \({\mathcal {V}}\subseteq \{p_1,\,p_2,\,p_3,\,p_4\}\), and \(\varphi _{\{\lnot p_2,\lnot p_3,p_4\}}\), \(\varphi _{\{p_1,\lnot p_2,p_4\}}\) and \(\varphi _{\{p_1,\lnot p_2,\lnot p_3,p_4\}}\) are different to \(\bigvee \varnothing \) because \({\mathcal {F}}\) models an extended-disjunctive program that has rules with \(\lnot p_2\vee \lnot p_3\vee p_4\) as head, rules with \(p_1\vee \lnot p_2\vee p_4\) as head, and rules with \(p_1\vee \lnot p_2\vee \lnot p_3\vee p_4\) as head, and no other rule whose head has at least \(\lnot p_2\) and \(p_4\) as disjuncts. Then the theory associated with a left shift completion of \({\mathcal {F}}\) would have as conditional alternative (a formula equivalent to):

Proposition 4.2

Two disjunctive programs such that one is a left shift completion of the other are logically \({\mathcal {S}}\)-equivalent.

Proof

Let disjunctive programs \({\mathcal {F}}=(\varphi _D)_{D\in \mathrm {Alt}({\mathcal {V}})}\) and \({\mathcal {F}}'=(\varphi '_D)_{D\in \mathrm {Alt}({\mathcal {V}})}\) be such that \({\mathcal {F}}'\) is a left shift completion of \({\mathcal {F}}\). Let \(D\in \mathrm {Alt}({\mathcal {V}})\) be given. Since \(\varphi '_D\) is logically \({\mathcal {S}}\)-equivalent to a condition of the form \(\bigvee \{\varphi _D\}\cup X\), \(\varphi '_D\rightarrow \bigvee \Box D\) logically \({\mathcal {S}}\)-implies \(\varphi _D\rightarrow \bigvee \Box D\). Moreover, for all members \(D'\) of \(\mathrm {Alt}({\mathcal {V}})\) with \(D'\supset D\), \(\{\bigwedge \Diamond \Box \mathord \sim (D'\setminus D),\bigvee \Box (D'\setminus D)\}\) is inconsistent. Hence \(\{\varphi _{D'}\rightarrow \bigvee \Box D'\mid D'\supseteq D\}\) logically \({\mathcal {S}}\)-implies \(\varphi '_D\rightarrow \bigvee \Box D\). We conclude that \({\mathcal {F}}\) and \({\mathcal {F}}'\) are logically \({\mathcal {S}}\)-equivalent. \(\square \)

Recall the illustrated defintion of an answer set at the beginning of Sect. 1.2. The definition of an answer set for an extended-disjunctive program is exactly the same; the fact that rule heads can be disjunctions rather than simple literals making absolutely no difference. That is, given an extended-disjunctive program \({\mathcal {R}}\), an answer set for \({\mathcal {R}}\) is a consistent set X of literals with the following property. Replace in (the bodies of the rules in) \({\mathcal {R}}\) all formulas of the form \({{\textit{not}\ }}\psi \) by \( true \) if \(\psi \notin X\), by \( false \) otherwise, and simplify, resulting in a set of rules, say \({\mathcal {R}}'\). Now for all atoms \(\alpha \), replace in \({\mathcal {R}}'\) all occurrences of \(\lnot \alpha \) by a new atom \(\alpha ^\star \), resulting in a new set of rules, say \({\mathcal {R}}''\). Then the set \(X^\star \) of members of X where all negated atoms of the form \(\lnot \alpha \) have been replaced by \(\alpha ^\star \), is the set of logical consequences of \(\mathcal R''\).

In Sect. 2.4, we saw how an answer set program \({\mathcal {R}}\) can be put in correspondence with a disjunctive program \({\mathcal {R}}^\star \). Clearly, every disjunctive program is of the form \({\mathcal {R}}^\star \) for some unique extended-disjunctive program \({\mathcal {R}}\) (generalised to allow countable disjunctions on the left hand sides of the rules). Hence answer sets can be defined on the basis of disjunctive programs rather than on the basis of extended-disjunctive programs, resulting in the definition that follows.

Definition 4.3

Let a disjunctive program \({\mathcal {F}}\) be given. An answer set for \({\mathcal {F}}\)is the set of claims in a member \(\mathfrak S\) of \({\mathcal {S}}\) with the following properties.

• \(\mathfrak S\) forces \(\mathrm {Th}({{\mathcal {F}}})\) and is \(Hyp({\mathcal {F}})\)-complete.

• For all \(\mathfrak T\in {\mathcal {S}}\), if \(\mathfrak T\) forces \(\mathrm {Th}({{\mathcal {F}}})\) and is \(Hyp({\mathcal {F}})\)-complete then the set of claims in \(\mathfrak T\) is not strictly included in the set of claims in \(\mathfrak S\).

It is easily verified that Definition 4.3 is equivalent to the standard definition, previously outlined, of an answer set. The verification amounts to rewriting an extended-disjunctive program \({\mathcal {R}}\) as a disjunctive program \({\mathcal {F}}\), essentially rewriting an occurrence in \({\mathcal {R}}\) of a literal \(\alpha \) not preceded by not as \(\Box \alpha \) in \({\mathcal {F}}\), and rewriting an occurrence in \({\mathcal {R}}\) of a formula of the form \({{\textit{not}\ }}\alpha \) or \({{\textit{not}\ }}\lnot \alpha \), with \(\alpha \) an atom, as \(\Diamond \Box \lnot \alpha \) or \(\Diamond \Box \alpha \) in \({\mathcal {F}}\), respectively. In effect, Definition 4.3 is nothing but the standard definition of an answer set modulo the mechanical translation, the mechanical rewriting, of an extended-disjunctive program as a disjunctive program.

To illustrate the need for the second condition in Definition 4.3 with a trivial example (that does not even need disjunction), the logic program \({{\textit{not}\ }}\lnot p\rightarrow q\), which has \(\{q\}\) as unique answer set, corresponds in our framework to a disjunctive program \({\mathcal {F}}\) with \(\mathrm {Th}({{\mathcal {F}}})=\{\Diamond \Box p\rightarrow \Box q\}\) and \(Hyp({\mathcal {F}})=\{\Diamond \Box p\}\). Then \(\mathfrak S=\{\Diamond \Box p,\Box q\}\) satisfies both conditions of the previous definition, whereas \(\{\Diamond \Box p,\Box q,\Box p\}\) and \(\{\Diamond \Box p,\Box q,\Box r\}\) satisfy only the first one (and have to be ruled out as \(\{q,r\}\) and \(\{q,p\}\) are not answer sets for \({{\textit{not}\ }}\lnot p\rightarrow q\)). Note that the “standard” left shift completion of a disjunctive program moves all subsets of literals in the head of a given clause to the left. For instance, the logic program \(\{p\rightarrow q,q\rightarrow p,p\vee q\}\) has as left shift completion:

with \(\{\Box p,\Box q\}\) as unique answer set.

The correspondence, discussed in Sect. 2, between answer sets and the sets of claims that are logical \({\mathcal {S}}\)-consequences of the theory associated with an associated disjunctive program complemented with a set of hypotheses constrained in a particular way, can now be fully formalised and established.

Definition 4.4

Let a disjunctive program \({\mathcal {F}}\) and a subset H of \(Hyp({\mathcal {F}})\) be given. We say that H is a complete hypothetical extension for \({\mathcal {F}}\)iff the set of stances \(\varphi \) such that \(\mathrm {Th}({{\mathcal {F}}})\cup H\vDash _{\mathcal {S}}\varphi \) is \(Hyp({\mathcal {F}})\)-complete.

Proposition 4.5

Let a disjunctive program \({\mathcal {F}}\), a left shift completion \({\mathcal {F}}'\) of \({\mathcal {F}}\), and a set X of claims be given. The following conditions are equivalent.

• X is an answer set for \({\mathcal {F}}\).

• There exists a complete hypothetical extension H for \({\mathcal {F}}'\) such that X is the set of claims that are logical \({\mathcal {S}}\)-consequences of \(\mathrm {Th}({{\mathcal {F}}'})\cup \{H\}\).

Proof

Suppose that X is an answer set for \({\mathcal {F}}\). Let \(\mathfrak S\) be a member of \({\mathcal {S}}\) that satisfies both items in Definition 4.3 and such that X is the set of claims in \(\mathfrak S\). Let H be the set of all hypotheses \(\Diamond \Box \varphi \) in \(Hyp({\mathcal {F}}')\) such that \(\mathfrak S\mathbin {\nVdash }\Box \mathord \sim \varphi \). Note that \(H\cap Hyp({\mathcal {F}})\) is equal to the set of hypotheses in \(\mathfrak S\cap Hyp({\mathcal {F}})\). Hence \(\mathfrak S\cup H\) forces \(\mathrm {Th}({{\mathcal {F}}})\cup H\), and by Proposition 4.2, also forces \(\mathrm {Th}({{\mathcal {F}}'})\cup H\). Moreover, for all \(\mathfrak T\in {\mathcal {S}}\) that force \(\mathrm {Th}({{\mathcal {F}}'})\cup H\), \(\mathfrak T\) is \(Hyp({\mathcal {F}})\)-complete, hence \(X\subseteq \mathfrak T\). Hence X is the set of claims that are logical \({\mathcal {S}}\)-consequences of \(\mathrm {Th}({{\mathcal {F}}'})\cup H\), and the set of stances \(\varphi \) such that \(\mathrm {Th}({{\mathcal {F}}'})\cup H\vDash _{\mathcal {S}}\varphi \) is trivially \(Hyp({\mathcal {F}}')\)-complete.

Conversely, let H be a complete hypothetical extension for \({\mathcal {F}}'\) such that X is the set of claims that are logical \({\mathcal {S}}\)-consequences of \(\mathrm {Th}({{\mathcal {F}}'})\cup H\). Obviously, \(X\cup H\) belongs to \({\mathcal {S}}\), forces \(\mathrm {Th}({{\mathcal {F}}})\) by Proposition 4.2, and is \(Hyp({\mathcal {F}})\)-complete since \(Hyp({\mathcal {F}})\) is a subset of \(Hyp({\mathcal {F}}')\). Also, every member \(\mathfrak T\) of \({\mathcal {S}}\) that forces \(\mathrm {Th}({{\mathcal {F}}})\) and contains H is such that all members of X are claims in \(\mathfrak T\). Hence X is an answer set for \({\mathcal {F}}\). \(\square \)

5.1 General strategy

We aim to show that given a disjunctive program \({\mathcal {F}}\) and a set H of hypotheses, a modification of the cut rule can be applied to H and any left shift completion of \({\mathcal {F}}\) and generate all alternatives that are logical \({\mathcal {S}}\)-consequences of \(\mathrm {Th}({{\mathcal {F}}})\cup H\), in such a way that properties (A)–(C) listed in Sect. 2 are satisfied. To this aim, we first introduce an intermediate proof system and demonstrate that it is complete; we refer to a proof in this system as a tableau proof. Then we will see how a tableau proof can be translated into a proof by cuts.

Tableau proofs are best represented as trees. Say that we try and derive an alternative of the form \(\bigvee \Box D\), \(D\in \mathrm {Alt}({\mathcal {V}})\), from a disjunctive program \({\mathcal {F}}\) and a set of hypotheses H. We build a tree T whose nodes are labeled with claims, except for the root and possibly some of the leaves. Let N be a node in T that has not been declared to be a leaf, and let X be the set of claims that label the nodes on the path from the root of T up to N. We try and select a conditional alternative R in the theory associated with a left shift completion of \({\mathcal {F}}\) whose condition is seen to be a logical \({\mathcal {S}}\)-consequence of \(H\cup X\). If R’s alternative is the empty disjunction, then N is given a nonlabelled child that is declared to be a leaf. If R’s alternative is of the form \(\bigvee \{\varphi _1,\dotsc ,\varphi _n\}\) for some \(n>0\) and pairwise distinct claims \(\varphi _1\), ..., \(\varphi _n\), then N is given n children labeled \(\varphi _1\), ..., \(\varphi _n\) and every child that receives a member of D as label is declared to be a leaf. If the construction eventually stops and results in a finite tree not consisting of its root only (this is guaranteed in case \({\mathcal {F}}\) is finite), then all leaves are unlabelled or labelled with nothing but members of D. For the tree to represent a successful tableau proof, D should be empty, in which case \(\mathrm {Th}({{\mathcal {F}}})\) is \({\mathcal {S}}\)-inconsistent with H, or at least one leaf should be labelled with a member of D. We will verify that it is always possible to build such a tree whenever \(\bigvee D\) is a logical consequence of \(\mathrm {Th}({{\mathcal {F}}})\cup H\), hence that the tableau proof procedure is complete.

5.2 Example

To illustrate both tableau proofs and proofs by cut, consider a disjunctive program \({\mathcal {F}}\) over the vocabulary \({\mathcal {V}}=\{p_0,\dotsc ,p_{10}\}\) such that \(\mathrm {Th}({{\mathcal {F}}})\) is logically \({\mathcal {S}}\)-equivalent to the set consisting of

and all conditional alternatives that follow.

It is easy to verify that \(\Box p_0\) is a logical \({\mathcal {S}}\)-consequence of \(\mathrm {Th}({{\mathcal {F}}})\) (it will be demonstrated in the detailed illustration of Sect. 6.2).

Let \((\varphi '_D)_{D\in \mathrm {Alt}({\mathcal {V}})}\) be a left shift completion of \({\mathcal {F}}\). It is clear that there is no point in left shifting a claim, say \(\Box \varphi \), from the right hand side to the left hand side of one of \(\mathrm {Th}({{\mathcal {F}}})\)’s conditional alternatives if \(\Box \mathord \sim \varphi \) does not occur on the right hand side of any other conditional alternative of \(\mathrm {Th}({{\mathcal {F}}})\). To simplify the matter further, let us ignore all left shifts that are not involved in the derivation of \(\Box p_0\) from \({\mathcal {F}}\) thanks to the tableau proof tree we are about to present. This allows us not to describe \(\varphi '_D\) for all \(D\in \mathrm {Alt}({\mathcal {V}})\), but only provide, for some members D of \(\mathrm {Alt}({\mathcal {V}})\), a condition that is logically \({\mathcal {S}}\)-equivalent to the disjunction of \(\varphi _D\) with the conditions of the form \(\bigwedge \Diamond \Box \mathord \sim (D'\setminus D)\) for those strict supersets \(D'\) of D, if any, such that the conditional alternative \(\varphi _{D'}\rightarrow \bigvee \Box (D'\setminus D)\) turns out to be useful. These considerations lead to writing down 9 relations of logical \({\mathcal {S}}\)-consequence:

and

The tree depicted next represents a tableau proof of \(\Box p_0\). It differs slightly from the general description we sketched at the beginning of the section, in that leaves with no label are not represented and additional information on the nodes is provided in the form of a finite set of numbers, whose meaning will be explained, and that will be needed to convert the tree into a proof by cuts. Also, it is technically more convenient to work with literals rather than claims. Finally, we stop referring to node labels, and rather adopt the usual definition of a tree, to be reminded shortly, as a finite sequence of entities, here literals; what was referred to above as the label of a node is now the last member of the sequence that defines that node.

The first level of T is determined by (2), and expresses that one of \(\Box p_1\), \(\Box \lnot p_2\), \(\Box p_3\), \(\Box p_4\) and \(\Box \lnot p_4\) holds. The node \((p_1,\lnot p_2)\) is determined by (4); its member of index 0 is \(p_1\), and \(\{\Box p_1\}\) is a \(\subseteq \)-minimal set of claims that logically \({\mathcal {S}}\)-implies \(\varphi '_{\{\lnot p_2\}}\), from which \(\Box \lnot p_2\) can be generated. The node \((p_1,\lnot p_2,p_3)\) is determined by (5); its member of index 1 is \(\lnot p_2\), and \(\{\Box \lnot p_2\}\) is a \(\subseteq \)-minimal set of claims that logically \({\mathcal {S}}\)-implies \(\varphi '_{\{p_3\}}\), from which \(\Box p_3\) can be generated. The node \((p_1,\lnot p_2,p_3)\) branches out into \((p_1,\lnot p_2,p_3,p_5)\), \((p_1,\lnot p_2,p_3,\lnot p_5)\), \((p_1,\lnot p_2,p_3,p_6)\) and \((p_1,\lnot p_2,p_3,p_7)\) as determined by (7); \(p_3\) is the element of index 2 of all those sequences, and \(\{\Box p_3\}\) is a \(\subseteq \)-minimal set of claims that logically \({\mathcal {S}}\)-implies \(\varphi '_{\{p_5,\lnot p_5,p_6,p_7\}}\), from which one of \(\Box p_5\), \(\Box \lnot p_5\), \(\Box p_6\) and \(\Box p_7\) is known to hold. The nodes \((p_1,\lnot p_2,p_3,p_5,p_0)\), \((p_1,\lnot p_2,p_3,\lnot p_5,p_0)\) and \((p_1,\lnot p_2,p_3,p_6,p_0)\) are all determined by (0); \(\{p_3,p_5\}\), \(\{p_3,\lnot p_5\}\) and \(\{p_3,p_6\}\) are the sets of elements of index 2 and 3 of these sequences, respectively, and if X denotes any of these sets then \(\Box X\) is a \(\subseteq \)-minimal set of claims that logically \({\mathcal {S}}\)-implies \(\varphi '_{\{p_0\}}\), from which \(\Box p_0\) is known to hold. We skip a few nodes and move to \((p_1,\lnot p_2,p_3,p_7,p_8)\); its members of index 2, 3 and 4 are \(p_3\), \(p_7\) and \(p_8\), and \(\{\Box p_3,\Box p_7,\Box p_8\}\) is a \(\subseteq \)-minimal set of claims that logically \({\mathcal {S}}\)-implies \(\varphi '_\varnothing \), indicating that \(\{\Box p_1,\Box \lnot p_2,\Box p_3,\Box p_7,\Box p_8\}\) cannot hold together and making \((p_1,\lnot p_2,p_3,p_7,p_8)\) a leaf of \(T'\). The subtrees of T rooted at \((\lnot p_2)\), \((p_3)\) and \((\lnot p_4)\) duplicate the subtrees rooted at \((p_1,\lnot p_2)\), \((p_1,\lnot p_2,p_3)\) and \((p_1,\lnot p_2,p_3,p_7,\lnot p_4)\), respectively, and are not explicitly represented; if they were depicted then of course, the integers associated with the nodes would have to be appropriately adapted. The tree T represents a tableau proof of \(\Box p_0\) because it has at least one leaf labeled with \(p_0\) (actually, it has 17 such leaves) and the remaining 5 leaves have no label (they are left unrepresented, and would extend four nodes ending in \(p_8\) and one node ending in \(p_{10}\)).

5.3 Completeness of the system of tableau proofs

Let us introduce all the terminology and notation relative to sequences and trees that will be needed in the sequel.

Notation 5.1

Given a sequence \(\sigma \), we denote by \(\mathrm {rng}(\sigma )\)—the range of \(\sigma \)—the set of members of \(\sigma \), by \(\mathrm {lt}(\sigma )\) the length of \(\sigma \), and in case \(\sigma \) is not the empty sequence, written (), by \(\mathrm {lst}(\sigma )\) the last element of \(\sigma \). Given a sequence \(\sigma \) and an element x, we denote by \(\sigma \star x\) the concatenation of \(\sigma \) with (x). Given a sequence \(\sigma \) and \(n\in \mathbb {N}\) with \(n\le \mathrm {lt}(\sigma )\), we denote by \(\sigma _{|n}\) the initial segment of \(\sigma \) of length n. Given a sequence \(\sigma \) and \(n\in \mathbb {N}\) with \(n<\mathrm {lt}(\sigma )\), we denote by \(\sigma (n)\) the \((n+1)\)-st element of \(\sigma \). Given a nonempty sequence \(\sigma \), we write \(\sigma ^-\) to denote \(\sigma \) truncated from its last element. Given two sequences \(\sigma \) and \(\tau \), we write \(\sigma \subseteq \tau \) to express that \(\sigma \) is an initial segment of \(\tau \).

Definition 5.2

Let a set X be given.

A tree over X is a set of finite sequences of members of X that is closed under initial segments.

Let a tree T over X be given. Note that () is the root of T. A inner node of T is a member of T that has a child in T, namely, a member of T of the form \(\sigma \star x\) for some \(x\in X\). A leaf of T is a member of T that is not an inner node of T. A branch of T is a \(\subseteq \)-maximal subset B of T with the property that any two members of B are such that one is an initial segment of the other.

Notation 5.3

Given a set X, a tree T over X, and a member \(\sigma \) of T, we let \({{\,\mathrm{Succ}\,}}_T(\sigma )\) denote the set of all \(x\in X\) with \(\sigma \star x\in T\).

It is time to fix the notation for substitution of stances in a condition by \(\bigwedge \varnothing \).

Notation 5.4

Let a condition \(\varphi \) and a set X of literals be given. We denote by \(\varphi [X]\) the result of substituting in \(\varphi \) all occurrences of the stances of the form \(\Box \xi \) or \(\Diamond \Box \xi \) with \(\xi \in X\) by \(\bigwedge \varnothing \). If X is a singleton \(\{\psi \}\) then we write \(\varphi [\psi ]\) rather than \(\varphi [X]\).

Let a condition \(\varphi \) and a set X of hypotheses and literals be given. Let Y be the set of literals in X. We denote by \(\varphi [X]\) the condition \(\psi [Y]\) where \(\psi \) is the result of substituting in \(\varphi \) all occurrences of all hypotheses in X by \(\bigwedge \varnothing \).

We can now define tableau proofs in accordance with the semi-formal description given at in Sect. 5.1.

Definition 5.5

Let a disjunctive program \({\mathcal {F}}=(\varphi _D)_{D\in \mathrm {Alt}({\mathcal {V}})}\), a set H of hypotheses, and a member D of \(\mathrm {Alt}({\mathcal {V}})\) be given. A tableau proof of D from \({\mathcal {F}}\) and H is a nonempty finite tree T over the set of literals with the following properties.

• For all branches B of T, \(H\cup \bigcup \{\Box \mathrm {rng}(\sigma )\mid \sigma \in B\}\) is consistent.

• No member of D occurs in any inner node of T.

• Let \(\sigma \) be a node of T. Then

• either \(\varphi _{{{\,\mathrm{Succ}\,}}_T(\sigma )}[H\cup \mathrm {rng}(\sigma )]\) is \({\mathcal {S}}\)-valid,

• or \({{\,\mathrm{Succ}\,}}_T(\sigma )=\varnothing \) and \(\sigma \) ends in a member of D.

The next proposition shows that the tableau proof procedure is sound and complete.

Proposition 5.6

Let a disjunctive program \({\mathcal {F}}\), a set H of hypotheses, a left shift completion \({\mathcal {F}}'\) of \({\mathcal {F}}\), and a member D of \(\mathrm {Alt}({\mathcal {V}})\) be given. Then \(H\cup \mathrm {Th}({{\mathcal {F}}})\vDash _{\mathcal {S}}\bigvee \Box D\) iff there exists a tableau proof of D from \({\mathcal {F}}'\) and H.

Proof

Let T be a tableau proof of D from \({\mathcal {F}}'\) and H. Let n be the number of inner nodes of T and leaves of T that do not end in a member of D (note that \(n>0\) whether or not T consists only of the empty sequence). Let \(X_1\), ..., \(X_n\) be sets of nodes of T such that \(X_1={{\,\mathrm{Succ}\,}}_T(())\) and for all nonzero \(i<n\), there exists \(\sigma \in X_i\) such that

• either \(\sigma \) is an inner node of T and \(X_{i+1}=X_i\cup \{\sigma \star \xi \mid \xi \in {{\,\mathrm{Succ}\,}}_T(\sigma )\}\setminus \{\sigma \}\),

• or \(\sigma \) is a leaf of T, \(\sigma \) does not end in a member of D, and \(X_{i+1}=X_i\setminus \{\sigma \}\).

Note that \(X_n\) is the set of leaves of T that end in a member of D; so in order to show that \(H\cup \mathrm {Th}({{\mathcal {F}}})\vDash _{\mathcal {S}}\bigvee \Box D\), it suffices to prove by Proposition 4.2 that \(H\cup \mathrm {Th}({{\mathcal {F}}'})\) logically \({\mathcal {S}}\)-implies \(\bigvee \bigl \{\bigwedge \Box \mathrm {rng}(\sigma )\mid \sigma \in X_n\bigr \}\) (from which we can derive that \({\mathcal {F}}\) is \({\mathcal {S}}\)-inconsistent with H in case \(X_n\) is empty). We prove by induction that for all nonzero \(i\le n\), \(H\cup \mathrm {Th}({{\mathcal {F}}'})\) logically \({\mathcal {S}}\)-implies \(\bigvee \bigl \{\bigwedge \Box \mathrm {rng}(\sigma )\mid \sigma \in X_i\bigr \}\). It is immediately verified that \(H\cup \mathrm {Th}({{\mathcal {F}}'})\) logically \({\mathcal {S}}\)-implies \(\bigvee \bigl \{\bigwedge \Box \mathrm {rng}(\sigma )\mid \sigma \in X_1\bigr \}\) (including if \(X_1=\varnothing \), which can only be the case if \({\mathcal {F}}\) is \({\mathcal {S}}\)-inconsistent with H). Let a nonzero \(i<n\) be given, and assume that \(H\cup \mathrm {Th}({{\mathcal {F}}'})\vDash _{\mathcal {S}}\bigvee \bigl \{\bigwedge \Box \mathrm {rng}(\sigma )\mid \sigma \in X_i\bigr \}\). Assume that \({\mathcal {F}}'\) is \({\mathcal {S}}\)-consistent with H, and let \(\mathfrak S\in {\mathcal {S}}\) force \(H\cup \mathrm {Th}({{\mathcal {F}}'})\). Suppose that \(X_{i+1}\) is of the form \(X_i\cup \{\tau \star \xi \mid \xi \in {{\,\mathrm{Succ}\,}}_T(\tau )\}\setminus \{\tau \}\) for some inner node \(\tau \) of T. It is immediately verified that if \(\mathfrak S\mathbin {\nVdash }\Box \mathrm {rng}(\tau )\) then \(\mathfrak S\mathbin {\Vdash }\bigvee \bigl \{\bigwedge \Box \mathrm {rng}(\sigma )\mid \sigma \in X_i\setminus \{\sigma \}\bigr \}\), and if \(\mathfrak S\mathbin {\Vdash }\Box \mathrm {rng}(\tau )\) then \(\mathfrak S\mathbin {\Vdash }\bigvee \bigl \{\bigwedge \Box \mathrm {rng}(\tau \star \xi )\mid \xi \in {{\,\mathrm{Succ}\,}}{\tau }\}\), hence \(\mathfrak S\) forces \(\bigvee \bigl \{\bigwedge \Box \mathrm {rng}(\sigma )\mid \sigma \in X_{i+1}\bigr \}\). Suppose that \(X_{i+1}\) is of the form \(X_i\setminus \{\tau \}\) for some leaf \(\tau \) of T that does not end in a member of D. Since \(\mathfrak S\) does not force \(\bigwedge \varnothing \rightarrow \bigvee \varnothing \), we infer that \(\mathfrak S\mathbin {\nVdash }\Box \mathrm {rng}(\tau )\), hence again, \(\mathfrak S\mathbin {\Vdash }\bigvee \bigl \{\bigwedge \Box \mathrm {rng}(\sigma )\mid \sigma \in X_{i+1}\bigr \}\), as wanted.

Conversely, assume that \(H\cup \mathrm {Th}({{\mathcal {F}}})\vDash _{\mathcal {S}}\bigvee \Box D\). Fix an enumeration \((D_i)_{i\in \mathbb {N}}\) of \(\mathrm {Alt}({\mathcal {V}})\). Set \({\mathcal {F}}'=(\varphi _E)_{E\in \mathrm {Alt}({\mathcal {V}})}\). Define a sequence \((T_n)_{n\in \mathbb {N}}\) of trees over the set of literals as follows. Set \(T_0=\{()\}\). Let \(n\in \mathbb {N}\) be given, and assume that \(T_n\) has been defined. First we let \(T_n\subseteq T_{n+1}\). Let \(\sigma \) be a leaf of \(T_n\). If \(\mathrm {rng}(\sigma )\cap D\ne \varnothing \) then no strict extension of \(\sigma \) belongs to \(T_{n+1}\). Suppose that \(\mathrm {rng}(\sigma )\cap D=\varnothing \). If there exists a least \(i\in \mathbb {N}\) such that \(H\cup \Box \mathrm {rng}(\sigma )\cup \Box D_i\) is consistent, \(\varphi _{D_i}[H\cup \mathrm {rng}(\sigma )]\) is \({\mathcal {S}}\)-valid and there is no initial segment \(\tau \) of \(\sigma \) such that \(\{\tau \star \xi \mid \xi \in D_i\}\subseteq T_n\), then the strict extensions of \(\sigma \) in \(T_{n+1}\) are precisely the sequences of the form \(\sigma \star \xi \) with \(\xi \in D_i\); otherwise no strict extension of \(\sigma \) belongs to \(T_{n+1}\). This completes the definition of \(T_{n+1}\). Set \(T=\bigcup _{n\in \mathbb {N}}T_n\). We are done if we show that T is a tableau proof of D from \({\mathcal {F}}'\) and H. Let B be a branch of T. We first show the following.

1. (1)

   B is finite.

2. (2)

   Let \(\sigma \) be the leaf of T that B ends in. If \(\mathrm {rng}(\sigma )\cap D=\varnothing \) then \(\varphi _\varnothing [H\cup \mathrm {rng}(\sigma )]\) is \({\mathcal {S}}\)-valid.

Suppose for a contradiction that either B is infinite or B is finite but (2) does not hold. Let X be the set of literals that occur in B. It is immediately verified that \(H\cup \Box X\) is consistent. Let \(\mathfrak S\) be the \(\subseteq \)-minimal member of \({\mathcal {S}}\) that contains \(H\cup \Box X\). Note that X contains no member of D whether B is finite or not, and so \(\mathfrak S\) does not force \(\bigvee \Box D\), whether D is empty or not. Let \(i\in \mathbb {N}\) be such that \(D=D_i\), so \(\mathfrak S\) forces \(\varphi _{D_i}\) . Let Y be the set of all literals \(\psi \) in \(D_i\) such that \(H\cup \Box X\cup \{\Box \psi \}\) is inconsistent. Let \(j\in \mathbb {N}\) be such that \(D_j=D_i\setminus Y\). Then by the choice of \({\mathcal {F}}'\), \(\mathfrak S\) forces \(\varphi _{D_j}\), and \(H\cup \Box X\cup \Box D_j\) is obviously consistent. It is then easy to verify that by assumption on B and by construction of \((T_n)_{n\in \mathbb {N}}\), there exists a member \(\tau \) of B with the property that:

• \(\varphi _{D_j}[H\cup \mathrm {rng}(\tau )]\) is \({\mathcal {S}}\)-valid;

• for all \(k<j\) and strict initial segments \(\tau '\) of \(\tau \), either \(\varphi _{D_k}[H\cup \mathrm {rng}(\tau ')]\) is not \({\mathcal {S}}\)-valid or \(\{\tau '\star \xi \mid \xi \in D_k\}\subseteq T\).

If \(D_j=\varnothing \) then B clearly ends in \(\tau \), which contradicts the assumption that (2) above does not hold. If \(D_j\ne \varnothing \) then \(\tau \star \xi \) belongs to B for some \(\xi \in D_j\) and \(\mathfrak S\) forces \(\bigvee \Box D_j\). So if \(\mathfrak S\) does not force \(\varphi _\varnothing \) then we infer that \(\mathfrak S\) forces \(H\cup \mathrm {Th}({{\mathcal {F}}'})\), which contradicts the assumption that \(H\cup \mathrm {Th}({{\mathcal {F}}'})\vDash _{\mathcal {S}}\bigvee \Box D\). So we have shown that B satisfies (A) and (B) above. In particular, we have shown that T contains no infinite branch, which by König’s lemma, implies that T is finite. Finally, from the construction of \((T_n)_{n\in \mathbb {N}}\) and the properties of T’s branches demonstrated above, we conclude that T is a tableau proof of D from \({\mathcal {F}}\) and H. \(\square \)

The next corollary emphasises that tableau proofs are suitable for refutation.

Corollary 5.7

Let a disjunctive program \({\mathcal {F}}\), a left shift completion \({\mathcal {F}}'\) of \({\mathcal {F}}\), and a set H of hypotheses be given. Then the following conditions are equivalent.

• \({\mathcal {F}}\) is \({\mathcal {S}}\)-inconsistent with H.

• There exists a tableau proof of \(\varnothing \) from \({\mathcal {F}}'\) and H.

It is well worth also to take note of both corollaries that follow, the second of which expresses the compactness of the tableau proof procedure.

Corollary 5.8

Let a disjunctive program \({\mathcal {F}}\), a left shift completion \({\mathcal {F}}'\) of \({\mathcal {F}}\), and a set H of hypotheses be such that \({\mathcal {F}}\) is \({\mathcal {S}}\)-consistent with H. Let a member D of \(\mathrm {Alt}({\mathcal {V}})\) be such that \(H\cup \mathrm {Th}({{\mathcal {F}}})\vDash _{\mathcal {S}}\bigvee \Box D\). Then every tableau proof of D from \({\mathcal {F}}'\) and H has at least one branch that ends in a member of D.

Corollary 5.9

Let a disjunctive program \({\mathcal {F}}\), a set H of hypotheses, and a member D of \(\mathrm {Alt}({\mathcal {V}})\) be such that \(H\cup \mathrm {Th}({{\mathcal {F}}})\vDash _{\mathcal {S}}\bigvee \Box D\). Let \({\mathcal {F}}'=(\varphi _E)_{E\in \mathrm {Alt}({\mathcal {V}})}\) be a left shift completion of \({\mathcal {F}}\). There exists a finite subset X of \(\mathrm {Alt}({\mathcal {V}})\) with the following property. Let \({\mathcal {F}}''=(\varphi _E)_{E\in \mathrm {Alt}({\mathcal {V}})}\) be the disjunctive program such that for all members E of \(\mathrm {Alt}({\mathcal {V}})\), either \(E\in X\) and \(\varphi '_E=\varphi _E\), or \(E\notin X\) and \(\varphi '_E=\bigvee \varnothing \). Then there exists a tableau proof of D from \({\mathcal {F}}''\) and H.

6.1 General strategy

Let us further exploit the example given in the previous section and explain, on the basis of that example, how a tableau proof can be converted into a proof by cuts. Let T be the tree depicted in the previous section, which, recall, represents a tableau proof of \(\Box p_0\). The strategy is to explore T depth first and label some nodes N in T with a member of \(\mathrm {Alt}({\mathcal {V}})\) determined by the (possibly empty) set of N’s children and by the labels associated with \(N_{|i_1+1}\), ..., \(N_{|i_k+k}\) where \(\{i_1,\dotsc ,i_k\}\) is the (possibly empty) set of numbers associated with N in T (those labels will necessarily exist). There might be subtrees of T that will be skipped during this exploration; the nodes of those subtrees will then not be labeled. Also, some nodes might receive various labels over time: when a leaf gets labeled, then the exploration of T proceeds by backtracking and the label assigned to that leaf replaces the label (guaranteed to exist) that had been previously assigned to the node we backtrack to. The fact that we will eventually obtain a proof of \(\Box p_0\) by cut will be captured by the fact that \(\Box p_0\) will be the label last assigned to a node. More generally, a proof by cut of an alternative of the form \(\bigvee \Box D\), \(D\in \mathrm {Alt}({\mathcal {V}})\), will require that the label last assigned to a node be a subset of D.

Let us explain in a little more detail how labels are determined. Let N be a node in T that has not received any label yet but whose parent, if any, has received some label. If N ends in \(p_0\) (more generally, if we try and prove \(\bigvee \Box D\) for some \(D\in \mathrm {Alt}({\mathcal {V}})\) and N ends in a member of D) then N is necessarily a leaf, and it receives the label last assigned to its parent. Suppose that we are not in that situation. If N has a parent and the label last assigned to it does not contain the literal N ends in, then the subtree of T rooted at N is skipped and none of its nodes receives any label. Suppose that we are not in that situation either. Let \(k\in \mathbb {N}\) and literals \(\xi _1\), ..., \(\xi _k\) be such that N has k children in T, those children being \(N\star \xi _1\), ..., \(N\star \xi _k\). Let \(n\in \mathbb {N}\) be the number of integers associated with N in T, and let \(i_1\), ..., \(i_n\) be those integers. Let \(\psi _1\), ..., \(\psi _n\) be the last elements of \(N_{|i_1}\), ..., \(N_{|i_n}\), and let \(D_1\), ..., \(D_n\) be the labels that have (necessarily) been assigned to \(N_{|i_1}\), ..., \(N_{|i_n}\), respectively (less precisely, \(\psi _1\), ..., \(\psi _n\) are the literals on the path from the root of T to N at positions \(i_0\), ..., \(i_n\), and \(D_1\), ..., \(D_n\) are the labels currently associated with those positions, respectively). Then \(\{\Box \psi _1,\dotsc ,\Box \psi _n\}\) is a \(\subseteq \)-minimal set of claims that logically \({\mathcal {S}}\)-implies \(\varphi _{\{\xi _1,\dots ,\xi _k\}}\), \(\psi _1\) belongs to \(D_1\), ..., and \(\psi _n\) belongs to \(D_n\). Hence the cut rule can be applied to \(\vdash \Box D_1\), ..., \(\vdash \Box D_n\) and \(\varphi _{\{\xi _1,\dotsc ,\xi _k\}}\vdash \Box \xi _1,\dotsc ,\Box \xi _k\). If \(\vdash \Box \chi _1,\dotsc ,\Box \chi _m\) is the consequent of that application of the cut rule, then \(\{\chi _1,\dotsc ,\chi _m\}\) is the label we first (and possibly last) assign to N.

6.2 Example

We will prove the completeness of the cut proof technique based on a construction which will deviate slightly from what has been outlined in that we will not assign labels to nodes in T (the tree used as an example), but rather define a new tree \(T'\) from T; the difference is purely technical. Following is a pictorial representation of \(T'\), together with some indication of how \(T'\) is constructed as we explore T depth first and backtrack from leaves to inner nodes down the tree. To save space, we represent a negated atom \(\varphi \) as \({\overline{\varphi }}\).

Let us explain how \(T'\) is obtained. Set \(\sigma _0=\{p_1,\lnot p_2,p_3,p_4,\lnot p_4\}\). The unique child of the root of \(T'\), namely \((\sigma _0)\), is determined by the successors of the root of T, similarly expressing that one of \(\Box p_1\), \(\Box \lnot p_2\), \(\Box p_3\), \(\Box p_4\) and \(\Box \lnot p_4\) holds. Set \(\sigma _1=\{\lnot p_2,p_3,p_4,\lnot p_4\}\). The node \((\sigma _0,\sigma _1)\) of \(T'\) is determined by the node \((p_1)\) of T, and more precisely, the associated number (namely, 0) and the successor (namely, \(\lnot p_2\)) of that node in T: \(\sigma _1\) is obtained by applying the cut rule as follows to \(\Box p_1\vee \Box \lnot p_2\vee \Box p_3\vee \Box p_4\vee \Box \lnot p_4\), which is currently associated with the element \((\sigma _0,\sigma _1)\) of index 0, and to \(\varphi '_{\{\lnot p_2\}}\rightarrow \Box \lnot p_2\).

Set \(\sigma _2=\{p_3,p_4,\lnot p_4\}\). The node \((\sigma _0,\sigma _1,\sigma _2)\) of \(T'\) is determined by the node \((p_1,\lnot p_2)\) of T, and more precisely, the associated number (namely, 1) and the successor (namely, \(p_3\)) of that node in T: \(\sigma _2\) is obtained by applying the cut rule as follows to \(\Box \lnot p_2\vee \Box p_3\vee \Box p_4\vee \Box \lnot p_4\), which is currently associated with the element \((\sigma _0,\sigma _1,\sigma _2)\) of index 1, and to \(\varphi '_{\{p_3\}}\rightarrow \Box p_3\).

In accordance with a depth-first exploration of \(T'\), set:

• \(\sigma _3=\{p_5,\lnot p_5,p_6, p_7,p_4,\lnot p_4\}\),

• \(\sigma _4=\{p_0,p_4,\lnot p_4,\lnot p_5, p_6, p_7\}\),

• \(\sigma _5=\{p_0,p_4,\lnot p_4, p_6, p_7\}\),

• \(\sigma _6=\{p_0,p_4,\lnot p_4, p_7\}\),

• ...,

• \(\sigma _{10}=\{\lnot p_9\}\),

• \(\sigma _{11}=\{p_0,\lnot p_1,p_{10},\lnot p_4\}\),

• ...,

• \(\sigma _{14}=\{p_0\}\).

Here is how \(\sigma _3\) is obtained.

Node \((\sigma _0,\sigma _1,\sigma _2,\sigma _3,\sigma _4)\) of \(T'\) is determined by node \((p_1,\lnot p_2,p_3,p_5)\) of T, and more precisely, the associated numbers (namely, 2 and 3) and the successor (namely, \(p_0\)) of that node in T: \(\sigma _4\) is obtained by applying the cut rule as follows, first to \(\Box p_3\vee \Box p_4\vee \Box \lnot p_4\), which is currently associated with the element \((\sigma _0,\sigma _1,\sigma _2,\sigma _3,\sigma _4)\) of index 2, second to \(\Box p_5\vee \Box \lnot p_5\vee \Box p_6\vee \Box p_7\vee \Box p_4\vee \Box \lnot p_4\), which is currently associated with the element \((\sigma _0,\sigma _1,\sigma _2,\sigma _3,\sigma _4)\) of index 3, and to \(\varphi '_{\{p_0\}}\rightarrow \Box p_0\).

As we backtrack one level up in T, we associate \(\Box p_0\vee \Box p_4\vee \Box \lnot p_4\vee \Box \lnot p_5\vee \Box p_6\vee \Box p_7\) in place of \(\Box p_5\vee \Box \lnot p_5\vee \Box p_6\vee \Box p_7\vee \Box p_4\vee \Box \lnot p_4\) to \((\sigma _0,\sigma _1,\sigma _2,\sigma _3)\). The node \((\sigma _0,\sigma _1,\sigma _2,\sigma _3,\sigma _5)\) of \(T'\) is determined by the node \((p_1,\lnot p_2,p_3,\lnot p_5)\) of T, and more precisely, the associated numbers (namely, 2 and 3) and the successor (namely, \(p_0\)) of that node in T: \(\sigma _5\) is obtained by applying the cut rule as follows, first to \(\Box p_3\vee \Box p_4\vee \Box \lnot p_4\), which is currently associated with the element \((\sigma _0,\sigma _1,\sigma _2,\sigma _3,\sigma _4)\) of index 2, second to \(\Box p_0\vee \Box p_4\vee \Box \lnot p_4\vee \Box \lnot p_5\vee \Box p_6\vee \Box p_7\), which is currently associated with the element \((\sigma _0,\sigma _1,\sigma _2,\sigma _3,\sigma _4)\) of index 3, and to \(\varphi '_{\{p_0\}}\rightarrow \Box p_0\).

As we backtrack one level up in T, we associate \(\Box p_0\vee \Box p_4\vee \Box \lnot p_4\vee \Box p_6\vee \Box p_7\) in place of \(\Box p_0\vee \Box p_4\vee \Box \lnot p_4\vee \Box \lnot p_5\vee \Box p_6\vee \Box p_7\) to \((\sigma _0,\sigma _1,\sigma _2,\sigma _3)\). Then \(\sigma _6\) is obtained as follows.

Moving on, \(\sigma _7\) and \(\sigma _8\) are obtained as follows.

Node \((\sigma _0,\sigma _1,\sigma _2,\sigma _3,\sigma _7,\sigma _9)\) of \(T'\) is determined by node \((p_1,\lnot p_2,p_3,p_7,p_8)\) of T, and more precisely, the associated numbers (namely, 2, 3 and 4) and the fact that that node has no successor in T: \(\sigma _9\) is obtained by applying the cut rule as follows, first to \(\Box p_3\vee \Box p_4\vee \Box \lnot p_4\), which is currently associated with the element \((\sigma _0,\sigma _1,\sigma _2,\sigma _3,\sigma _7,\sigma _9)\) of index 2, second to \(\Box p_0\vee \Box p_4\vee \Box \lnot p_4\vee \Box p_7\), which is currently associated with the element \((\sigma _0,\sigma _1,\sigma _2,\sigma _3,\sigma _7,\sigma _9)\) of index 3, third to \(\Box p_0\vee \Box p_4\vee \Box p_8\), which is currently associated with the element \((\sigma _0,\sigma _1,\sigma _2,\sigma _3,\sigma _7,\sigma _9)\) of index 4, and to \(\varphi '_\varnothing \rightarrow \bigvee \varnothing \).

The node of T that comes after \((p_1,\lnot p_2,p_3,p_7,p_8)\) in a depth-first exploration of T is \((\lnot p_2)\), but as \(\lnot p_2\) does not occur in \(\sigma _9\), the subtree of T rooted at \((\lnot p_2)\) is skipped over. The next node of T that is then reached in a depth-first exploration of T is \((p_3)\), that also does not occur in \(\sigma _9\), so the subtree of T rooted at \((p_3)\) is skipped over. The next node of T to consider is then \((p_4)\), and as \(p_4\) belongs to \(\sigma _9\), we associate \(\Box p_0\vee \Box p_4\vee \Box \lnot p_4\) in place of \(\Box p_1\vee \Box \lnot p_2\vee \Box p_3\vee \Box p_4\vee \Box \lnot p_4\) to \((\sigma _0)\). As the condition of \(\varphi '_{\lnot p_9}\) is \(\bigwedge \varnothing \), no application of the cut rule is necessary to determine \(\sigma _{10}\). Then \(\sigma _{11}\), \(\sigma _{12}\) and \(\sigma _{13}\) are determined as follows.

Finally, \(\sigma _{14}\) is found out to be equal to \(\{p_0\}\) thanks to the following application of the cut rule, completing the proof by cuts that \({\mathcal {F}}\) logically \({\mathcal {S}}\)-implies \(\Box p_0\).

6.3 Condition reduction

In Sect. 2.5, we discussed how the substitution of stances in a condition by \(\bigwedge \varnothing \) could be mechanically processed to eventually result in \(\bigwedge \varnothing \) precisely in case the condition with those substitutions performed was \({\mathcal {S}}\)-valid. This is a particular case of the reduction of a condition with stances substituted by \(\bigwedge \varnothing \) into a simpler condition, in a way captured by the couple of definitions that follow.

Definition 6.1

Let a condition \(\varphi \) be given. We call reduct of \(\varphi \) any condition \(\psi \) such that one of the conditions that follow holds.

• \(\psi \) is \(\varphi \).

• \(\varphi \) is of the form \(\bigvee X\cup \{\bigvee Y\}\) and \(\psi \) is \(\bigvee X\cup Y\).

• \(\varphi \) is of the form \(\bigwedge X\cup \{\bigwedge Y\}\) and \(\psi \) is \(\bigwedge X\cup Y\).

• \(\varphi \) is of the form \(\bigvee X\cup \{\bigwedge \varnothing \}\) and \(\psi \) is \(\bigwedge \varnothing \).

• \(\varphi \) is of the form \(\bigwedge X\cup \{\bigvee \varnothing \}\) and \(\psi \) is \(\bigvee \varnothing \).

• \(\varphi \) is of the form \(\bigvee X\cup \{\xi \}\) and \(\psi \) is \(\bigvee X\cup \{\chi \}\) for some reduct \(\chi \) of \(\xi \).

• \(\varphi \) is of the form \(\bigwedge X\cup \{\xi \}\) and \(\psi \) is \(\bigwedge X\cup \{\chi \}\) for some reduct \(\chi \) of \(\xi \).

Definition 6.2

A condition is said to be in reduced form iff it is its only reduct.

Property 6.3

Every condition has a unique reduct in reduced form.

Notation 6.4

Given a condition \(\varphi \), we let \(\rho (\varphi )\) denote the unique condition in reduced form that is a reduct of \(\varphi \).

For an example, if \(\varphi \) is the condition defined at the beginning of the last paragraph of Sect. 2.5, then the discussion in that paragraph shows that \(\rho (\varphi )=\bigwedge \varnothing \).

Property 6.5

For all conditions \(\varphi \), \(\rho (\varphi )\) is logically \({\mathcal {S}}\)-equivalent to \(\varphi \).

The key feature that a \({\mathcal {S}}\)-valid condition can be reduced to \(\bigwedge \varnothing \) is a corollary of the property that follows.

Property 6.6

Let a condition \(\varphi \) and a set X of hypotheses and literals be given. Let \(\mathfrak S\) be the \(\subseteq \)-minimal member of \({\mathcal {S}}\) that contains all hypotheses in X and all claims of the form \(\Box \xi \) with \(\xi \in X\). Then \(\mathfrak S\) forces \(\varphi \) iff \(\rho (\varphi [X])\) is equal to \(\bigwedge \varnothing \).

Corollary 6.7

For all conditions \(\varphi \), if \(\varphi \) is \({\mathcal {S}}\)-valid then \(\rho (\varphi )\) is \(\bigwedge \varnothing \).

6.4 Completeness of the system of proofs by cuts

What can be derived from a disjunctive program and a set of hypotheses by applying the cut rule iteratively is defined in the notation that follows. It formalises the notation \([{\mathcal {F}},H]\) which had been informally introduced towards the end of Sect. 2.4, and essentially captures the notion of proof by application of a suitable form of the cut rule, identified in our discussion of Sect. 2.

Notation 6.8

Let a disjunctive program \({\mathcal {F}}=(\varphi _D)_{D\in \mathrm {Alt}({\mathcal {V}})}\) and a set H of hypotheses be given. We define \([{\mathcal {F}},H]\) as the \(\subseteq \)-minimal set of members of \(\mathrm {Alt}({\mathcal {V}})\) of the form \(D\cup (D_1\setminus \{\psi _1\})\cup \dots \cup (D_k\setminus \{\psi _k\})\) such that

• k belongs to \(\mathbb {N}\), D to \(\mathrm {Alt}({\mathcal {V}})\), each of \(D_1\), ..., \(D_k\) to \([{\mathcal {F}},H]\), and \(\psi _1\), ..., \(\psi _k\) are literals in \(D_1\), ..., \(D_k\), respectively,

• \(\psi _1\), ..., \(\psi _k\) all occur in \(\varphi _D[H]\), and

• \(\rho \bigl (\varphi _D[H\cup \{\psi _1,\dotsc ,\psi _k\}]\bigr )=\bigwedge \varnothing \).

The cut rule is valid:

Proposition 6.9

For all disjunctive programs \({\mathcal {F}}\), sets H of hypotheses and members D of \([{\mathcal {F}},H]\), \(\bigvee D\) is a logical \({\mathcal {S}}\)-consequence of \(H\cup \mathrm {Th}({{\mathcal {F}}})\).

Proof

Let a disjunctive program \({\mathcal {F}}=(\varphi _D)_{D\in \mathrm {Alt}({\mathcal {V}})}\) and a set H of hypotheses be given. Let \(D\in \mathrm {Alt}({\mathcal {V}})\), \(k\in \mathbb {N}\), members \(D_1\), ..., \(D_k\) of \([{\mathcal {F}},H]\), and literals \(\psi _1\), ..., \(\psi _k\) in \(D_1\), ..., \(D_k\), respectively, be such that \(\psi _1\), ..., \(\psi _k\) all occur in \(\varphi _D[H]\) and \(\rho \bigl (\varphi _D[H\cup \{\psi _1,\dotsc ,\psi _k\}]\bigr )=\bigwedge \varnothing \). Set \(D'=D\cup (D_1\setminus \{\psi _1\})\cup \dots \cup (D_k\setminus \{\psi _k\})\). Let \(\mathfrak S\in {\mathcal {S}}\) force \(H\cup \mathrm {Th}({{\mathcal {F}}})\) and each of \(\bigvee \Box D_1\), ..., \(\bigvee \Box D_k\). If \(\mathfrak S\) does not force all of \(\Box \psi _1\), ..., \(\Box \psi _k\), then \(\mathfrak S\) forces \(\bigvee D_i\setminus \{\psi _i\}\) for some nonzero \(i\le k\), hence \(\bigvee \Box D'\). Suppose that \(\mathfrak S\) forces all of \(\Box \psi _1\), ..., \(\Box \psi _k\). Since \(\mathfrak S\mathbin {\Vdash }H\) and \(\rho \bigl (\varphi _D[H\cup \{\psi _1,\dotsc ,\psi _k\}]\bigr )=\bigwedge \varnothing \), then \(\mathfrak S\) forces \(\varphi _D\). Since also \(\mathfrak S\mathbin {\Vdash }\mathrm {Th}({{\mathcal {F}}})\) then \(\mathfrak S\) forces \(\bigvee \Box D\), hence \(\bigvee \Box D'\). \(\square \)

We can finally formulate and prove the key result of this paper.

Proposition 6.10

Let a disjunctive program \({\mathcal {F}}\), a left shift completion \({\mathcal {F}}'\) of \({\mathcal {F}}\), and a set H of hypotheses be given. Then for all \(D\in \mathrm {Alt}({\mathcal {V}})\), \(\bigvee \Box D\) is a logical \({\mathcal {S}}\)-consequence of \(H\cup \mathrm {Th}({{\mathcal {F}}})\) iff \([{\mathcal {F}}',H]\) contains a subset of D.

Proof

Set \({\mathcal {F}}'=(\varphi _E)_{E\in \mathrm {Alt}({\mathcal {V}})}\). By Proposition 5.6, let T be a tableau proof of D from \({\mathcal {F}}'\) and H. Let \(T'\) be the set of members of T that contain no occurrence of any member of D. Let \(N\in \mathbb {N}\) be the cardinality of \(T'\), and let \((\sigma _0,\dots ,\sigma _{N-1})\) be an enumeration of the members of \(T'\) such that \(\sigma _0=()\) and for all \(i<N\), \(\sigma _i\) is a child of a member of \(\{\sigma _j\mid j<i\}\) in \(T'\) of maximal length (so \((\sigma _i)_{i<N}\) is a depth-first enumeration of \(T'\)). For all \(n\in \mathbb {N}\) and for all members \(\sigma \) of \(T'\) of length n, we let \(\mathrm {spt}(\sigma )\)—the support of \(\sigma \)—denote a \(\subseteq \)-minimal subset of \(\{0,\dotsc ,n-1\}\) such that \(\varphi _{{{\,\mathrm{Succ}\,}}_T(\sigma )}[H\cup \{\sigma (i)\mid i\in \mathrm {spt}(\sigma )\}]\) is \({\mathcal {S}}\)-valid (it is immediately verified that such a set exists). We now inductively define for all \(i<N\) a sequence \(([\sigma _i])_{i<N}\) of members of \(\mathrm {Alt}({\mathcal {V}})\) of length either 0 or \(\mathrm {lt}(\sigma _i)+1\). Set \([\sigma _0]=({{\,\mathrm{Succ}\,}}_T(\sigma _0))\). Let a nonzero \(i<N\) be least such that \([\sigma _i]\) has not been defined yet. Then by construction, \([\sigma _{i-1}]\ne ()\). We now determine some integer j with \(i\le j<N\) and define \([\sigma _k]\) for all \(k\in \{i,\dotsc ,j\}\). Let j be the least integer such that either \(j=N\), or \(i\le j<N\), \(\mathrm {lt}(\sigma _j)\le \mathrm {lt}(\sigma _i)\), and \(\mathrm {lst}(\sigma _j)\in \mathrm {lst}([\sigma _{i-1}])\). Then for all \(k\in \{i,\dotsc ,j-1\}\), \([\sigma _k]=()\). If \(j=N\) then we are done with the construction, so suppose otherwise. Note that for all strict initial segments \(\tau \) of \(\sigma _j\), \([\tau ]\) has been defined and is different to ().

• If \(\mathrm {lt}(\sigma _j)>1\) then \([\sigma _j]_{|\mathrm {lt}(\sigma _j)-1}\) is equal to \([\sigma _{i-1}]_{|\mathrm {lt}(\sigma _j)-1}\).

• The penultimate element of \([\sigma _j]\) is equal to \(\mathrm {lst}([\sigma _{i-1}])\).

• \(\mathrm {lst}([\sigma _j])\) is equal to \({{\,\mathrm{Succ}\,}}_T(\sigma _j)\cup \bigcup \bigl \{[\sigma _j](n)\setminus {\sigma _j(n)}\bigm | n\in \mathrm {spt}(\sigma _j)\bigr \}\).

We prove by induction that the following holds for all \(i<N\) with \([\sigma _i]\ne ()\).

1. (1)

   For all \(n<\mathrm {lt}(\sigma _i)\), \([\sigma _i](n)\) is included in the union of \(D\cup \{\sigma _i(n)\}\) with \(\{\mathrm {lst}(\sigma _j)\mid i< j<N,\, \mathrm {lt}(\sigma _j)\le n+1,\, \sigma _j^-\subseteq \sigma _i\}\).

2. (2)

   \(\mathrm {lst}([\sigma _i])\subseteq D\cup \{\mathrm {lst}(\sigma _j)\mid i< j<N,\, \mathrm {lt}(\sigma _j)\le \mathrm {lt}(\sigma _i)+1,\ \sigma _j^-\subseteq \sigma _i\}\).

Verification of (1) and (2) is straightforward for \(i=0\). Let \(k<N\) be such that \([\sigma _k]\ne ()\), and assume that for all \(i<k\) with \([\sigma _i]\ne ()\), (1) and (2) hold. Let i be the maximal integer smaller than k such that \([\sigma _i]\ne ()\). If \(\mathrm {lt}(\sigma _k)>1\) then, using part (1) of the inductive hypothesis, the fact that \((\sigma _j)_{j<N}\) is a depth-first enumeration of \(T'\), and the definition of \([\sigma _k]_{|\mathrm {lt}(\sigma _k)-1}\), it is easy to verify the following.

(\(\dagger \))   For all \(n<\mathrm {lt}(\sigma _k)-1\), \([\sigma _k](n)\) is included in

$$\begin{aligned} D\cup \{\sigma _k(n)\}\cup \{\mathrm {lst}(\sigma _j)\mid k< j<N,\, \mathrm {lt}(\sigma _j)\le n+1,\,\sigma _j^-\subseteq \sigma _k\}. \end{aligned}$$

Using part (2) of the inductive hypothesis, the fact that \((\sigma _j)_{j<N}\) is a depth-first enumeration of \(T'\), and the fact that the penultimate element of \([\sigma _k]\) is \(\mathrm {lst}([\sigma _i)\)], it is easy to verify the following, wether \(\mathrm {lt}(\sigma _k)=\mathrm {lt}(\sigma _i)+1\) or whether \(\mathrm {lt}(\sigma _k)\le \mathrm {lt}(\sigma _i)\).

(\(\ddagger \))   \([\sigma _k](\mathrm {lt}(\sigma _k)-1)\) is included in

$$\begin{aligned} D\cup \{\sigma _k(\mathrm {lt}(\sigma _k)-1)\}\cup \{\mathrm {lst}(\sigma _j)\mid k< j<N,\, \mathrm {lt}(\sigma _j)\le \mathrm {lt}(\sigma _k),\,\sigma _j^-\subseteq \sigma _k\}. \end{aligned}$$

Finally, using (\(\dagger \)) and (\(\ddagger \)) and the definition of \(\mathrm {lst}([\sigma _k])\), it is easy to verify that

So (1) and (2) hold for all \(i<N\) with \([\sigma _i]\ne ()\). From (2) and the definition of \((\sigma _i)_{i<N}\), we then infer that for all \(i<N\), if \(\mathrm {lst}([\sigma _i])\nsubseteq D\) then there exists \(j<N\) with \(i<j\) and \([\sigma _j]\ne ()\). But this obviously implies the following.

There exists \(i<N\) with \([\sigma _i]\ne ()\) and \(\mathrm {lst}([\sigma _i])\subseteq D\).

To complete the proof of the proposition, it suffices to show that for all \(i<N\) with \([\sigma _i]\ne ()\), \(\mathrm {lst}([\sigma _i])\) belongs to \([{\mathcal {F}}',H]\). Proof is by induction. Trivially, \(\mathrm {lst}([\sigma _0])\) is a member of \([{\mathcal {F}}',H]\). Let \(i<N\) be such that \([\sigma _i]\ne ()\) and for all \(j<i\) with \([\sigma _j]\ne ()\), \(\mathrm {lst}([\sigma _j])\in [{\mathcal {F}}',H]\). Note that for all \(n<\mathrm {lt}(\sigma _i)\), there exists \(j<i\) with \([\sigma _j]\ne ()\) and \([\sigma _i](n)\) is equal to \(\mathrm {lst}([\sigma _j])\). Let \(k\in \mathbb {N}\) denote the cardinality of \(\mathrm {spt}(\sigma _i)\), and let \(e_1\), ..., \(e_k\) enumerate its elements. By definition of \(\mathrm {spt}(\sigma _i)\) (and more particularly, the \(\subseteq \)-minimality condition), \(\varphi _{\mathrm {lst}(\sigma _i)}[H]\) contains at least one occurrence of each of \(\Box \sigma _i(e_1)\), ..., \(\Box \sigma _i(e_k)\). Also note that for all nonzero \(j\le k\), \(\sigma _i(k)\) belongs to \([\sigma _i](k)\), and that \(\varphi _{\mathrm {lst}(\sigma _i)}[H\cup \{[\sigma _i](e_1),\dotsc ,[\sigma _i](e_k)\}]\) is \({\mathcal {S}}\)-valid. We conclude from the previous observations and the definitions of \([{\mathcal {F}}',H]\) and \(\mathrm {lst}([\sigma _i])\) that \([{\mathcal {F}}',H]\) contains \(\mathrm {lst}([\sigma _i])\), completing the proof of the proposition. \(\square \)

We have presented a classical, modal approach to disjunctive logic programs. It is classical in three respects. First, in that only classical negation is used. Second, in that a classical proof technique, based on a generalisation of the cut rule, is complete. Third, in that the semantics can be defined in terms of logical consequence, rather than in terms of minimal or preferred models. The semantics is flexible enough to capture the well known semantics that have been proposed, by possibly expanding the set of rules with formulas referred to as hypotheses, requested to satisfy some special conditions. This has been demonstrated for the answer set semantics.