A Tableaux Calculus for Default Intuitionistic Logic

Abstract

We build a Default Logic variant on Intuitionistic Propositional Logic and develop a sound, complete, and terminating, tableaux calculus for it. We also present an implementation of the calculus. We motivate and illustrate the technical elements of our work with examples.

1 Introduction

Non-monotonic formalisms have traditionally been defined with a classical semantics [20]. More recently –following the seminal work of Gabbay [19]– there is an interest in the interplay between non-monotonic formalisms and Intuitionistic Logic (IL). E.g., in [38] a formalization of a notion of non-monotonic implication capturing non-monotonic consequence based on IL is proposed; in [39] the work of Gabbay in [19] is revised; in [30] a characterization of answer sets for logic programs with nested expressions is offered in terms of provability in IL (generalizing earlier proposals of Pearce in [32, 33]). The articles just mentioned have in common a study of the interplay between non-monotonic formalisms and IL from a theoretical perspective. Another interesting take on this interplay can be found in the area of Normative Systems or Legal Artificial Intelligence. E.g., in [22] a Description Logic built on IL is presented as a way to deal with conflicts present in laws and normative systems. These conflicts usually lead to logical inconsistencies when they are formally analyzed, bringing to the fore the need for an adequate semantics for negation in such a context. Another example is [31], where a construction of an I/O Logic –a general framework to study and reason about conditional norms [28]– is carried out on IL.

The interplay between non-monotonic formalisms and IL in normative systems is succinctly illustrated by the following motivating example (adapted from [26]). Let the possible outcomes of a trial be the verdicts of guilty or not guilty. A verdict of guilty is obtained when the evidence presented by the prosecution meets the so-called “beyond reasonable doubt” standard of proof. A verdict of not guilty is obtained when the evidence fails to meet said standard of proof; say because the defense manages to pinpoint contradictions in what the prosecution has presented. In such a context, the proposition guilty or not guilty is not understood as plainly true. Associated to it there is a proof of guiltiness; or a proof that this leads to contradictions. This intuitive understanding of guilty or not guilty departs from its classical interpretation and better fits in an intuitionistic setting.

Furthermore, as stated in [26], a proposition such as: a verdict of guilty implies not innocent is intuitively correct. The reason for this is that a verdict of guilty, as mentioned, is backed up by evidence meeting a standard of proof “beyond reasonable doubt”, and such a proof can be used to convert any proof of innocent into a contradiction. But we might be more reluctant to accept the contraposition: innocent implies not guilty as intuitively correct. Being innocent, as a concept, is not backed up by any notion of evidence, neither it has to meet any standard of proof. A common starting point of a trial is the so-called principle of presumption of innocence, whereby someone accused of committing a crime is a priori innocent. In other words, some care needs to be taken in an intuitionistic setting for the law of contraposition does not necessarily hold.

The principle of presumption of innocence is clearly defeasible. If we only know that a person has been accused of committing a crime, we must conclude that this person is innocent. However, if additional information is brought up, e.g., a credible witness, the murder weapon, etc., the principle ceases to apply and the conclusion that the person is innocent is withdrawn. In other words, the principle of presumption of innocence behaves non-monotonically.

Here, we build a default logic over Intuitionistic Propositional Logic ($\mathsf {IPL}$). Our aim is to formally reason about scenarios such as the one presented above. The choice of a default logic is not arbitrary. Since their introduction in [37], it has become clear that default logics have a special status in the literature on non-monotonic logic due to a relatively simple syntax and semantics, natural representation capabilities, and direct connections to other non-monotonic logics [2, 5]. From a logic engineering point of view default logics are also interesting since they can be modularly built on an underlying logic having some minimal properties [8]. Moreover, we develop a tableaux calculus for our default logic taking some ideas from [7, 9]. The resulting calculus is sound, complete, and terminating. Not many proof calculi for default logics built over IL exist. Important works are [1, 14]. In [1], a tableaux method is presented for a default logic built on $\mathsf {IPL}$ which allows for the computation of extensions, but not for checking default consequence. The latter is covered in [14], where a sequent calculus is presented. The calculi introduced in [1, 14] are related to ours but differ in some important aspects, in particular, in their construction. In addition, we present a prototype implementation which enables automated reasoning, a feature missing in [1, 14].

Structure. In Sect. 2 we introduce preliminary definitions and results. More precisely, we present Intuitionistic Propositional Logic ($\mathsf {IPL}$), and a default logic built over $\mathsf {IPL}$ ($\mathscr {D}\mathsf {IPL}$). In Sect. 3 we recall tableaux for $\mathsf {IPL}$ and develop a tableaux calculus for default consequence in $\mathscr {D}\mathsf {IPL}$. In Sect. 4 we present an implementation of our calculus. In Sect. 5 we report on a preliminary empirical evaluation of our implementation. In Sect. 6 we conclude the paper and discuss future research.

2 Basic Definitions

This section introduces basic definitions to make the paper self-contained.

Intuitionistic Logic. The syntax and semantics of Intuitionistic Propositional Logic ($\mathsf {IPL}$) is defined below.

Definition 1

(Syntax). The set $\mathscr {F}$ of wffs of $\mathsf {IPL}$ is defined on an enumerable set of proposition symbols, and is determined by the grammar

$$ \varphi \,{::=}\, p_i \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \lnot \varphi \mid \varphi \supset \varphi . $$

We write $\bot$ as an abbreviation for $p\wedge \lnot p$, and $\top$ for $\lnot \bot$.

As in [35], we define the semantics for $\mathsf {IPL}$ via intuitionistic Kripke models.

Definition 2

(Models). A Kripke model $\mathfrak {M}$ is a tuple $\langle W, \preccurlyeq , V\rangle$ where: W is a non-empty set of elements (a.k.a. worlds); ${\preccurlyeq }\subseteq {W \times W}$ is the accessibility relation; and $V: {W \rightarrow 2^\mathscr {P}}$ is the valuation function. An intuitionistic Kripke model is a Kripke model $\mathfrak {M}$ in which $\preccurlyeq$ is reflexive and transitive, and in which V satisfies the so-called heredity condition: for all $w \preccurlyeq w'$, if $w\in V(p)$, $w'\in V(p)$.

Definition 3

(Semantics). Let $\mathfrak {M}= \langle W, \preccurlyeq , V \rangle$ be an intuitionistic Kripke model, $w \in W$, and $\varphi \in \mathscr {F}$, we define the satisfiability relation ${\mathfrak {M}, w} \,\models \, \varphi$ s.t.:

$$ \begin{array}{l c l} \mathfrak {M}, w \,\models \, p &{} \hbox { iff } &{} p \in V(w) \\ \mathfrak {M}, w \,\models \, \varphi \wedge \psi &{} \hbox { iff } &{} \mathfrak {M}, w \,\models \, \varphi \hbox { and } \mathfrak {M}, w \,\models \, \psi \\ \mathfrak {M}, w \,\models \, \varphi \vee \psi &{} \hbox { iff } &{} \mathfrak {M}, w \,\models \, \varphi \hbox { or } \mathfrak {M}, w \,\models \, \psi \\ \mathfrak {M}, w \,\models \, \lnot \varphi &{} \hbox { iff } &{} \hbox {for all } w \preccurlyeq w', \ {\mathfrak {M}, w' \,\nvDash \, \varphi } \\ \mathfrak {M}, w \,\models \, \varphi \supset \psi &{} \hbox { iff } &{} \hbox {for all } w \preccurlyeq w', \hbox { if } {\mathfrak {M}, w' \,\models \, \varphi } \hbox { then } \mathfrak {M},w'\,\models \,\psi . \end{array} $$

Notice that, unlike Classical Propositional Logic, $\mathfrak {M},w\,\nvDash \,\varphi$ is not equivalent to $\mathfrak {M},w\,\models \,\lnot \varphi$. For any $\varPhi \subseteq \mathscr {F}$, we say that $\mathfrak {M},w\,\models \,\varPhi$ iff $\mathfrak {M},w\,\models \,\varphi$, for all $\varphi \in \varPhi$.

Next, we introduce the definition of consequence for $\mathsf {IPL}$.

Definition 4

(Consequence). Let $\varPhi \subseteq \mathscr {F}$ and $\varphi \in \mathscr {F}$; we say that $\varphi$ is a logical consequence of $\varPhi$, notation , iff for every $\mathfrak {M}$ and w in $\mathfrak {M}$, if ${{\mathfrak {M}, w} \,\models \, \varPhi }$, then ${{\mathfrak {M}, w} \,\models \, \varphi }$¹. We use as an abbreviation for . We say that $\varPhi$ is consistent if , otherwise it is inconsistent.

It is well known that satisfies reflexivity, monotonicity, cut, structurality and compactness (see e.g. [18] for details). In Definition 4 consequence in $\mathsf {IPL}$ is characterized semantically in terms of Kripke models. In Sect. 3 we present a syntactic characterization based on a proof system.

Default Logic. First introduced in [37], Default Logic comprises a sub-class of non-monotonic logics, characterized by so-called defaults and extensions. A default is a 3-tuple of formulas, notation . Intuitively, we can think of a default as a defeasible conditional which given some conditions on $\pi$ and $\rho$ enables us to obtain $\chi$. Extensions formalize what are these conditions. Defaults and extensions are introduced below.

Definition 5

(Defaults and Default Theories). We call ${\mathscr {D}= \mathscr {F}^3}$ the set of all defaults. Let $\varDelta \subseteq \mathscr {D}$, , and . A default theory ${\Theta }$ is a pair where $\varPhi \subseteq \mathscr {F}$ and $\varDelta \subseteq \mathscr {D}$. For any default theory ${\Theta }= (\varPhi , \varDelta )$, we define and .

In what follows we restrict our attention to finite default theories, i.e., default theories ${\Theta }$ in which both and are finite sets. Though our definitions extend directly to infinite default theories, there are some subtleties involved in dealing with infinite sets of defaults which we wish to avoid here (see [8] for details).

Definition 6

(Triggered). Let ${\Theta }$ be a default theory, and ; we say that $\delta$ is triggered by $\varDelta$ iff .

Definition 7

(Blocked). Let ${\Theta }$ be a default theory, and ; we say that $\delta$ is blocked by $\varDelta$ iff there is s.t. is inconsistent.

Definition 8

(Detached). Let ${\Theta }$ be a default theory and ; we say that $\delta$ is detached by $\varDelta$ if $\delta$ is triggered and not blocked by $\varDelta$.

Intuitively, for a default in the context of a default theory ${\Theta }$, the notion of detachment in Definition 8 tells us under which conditions on $\pi$ and $\rho$ we can obtain $\chi$. The definition of detachment is an intermediate step towards the definition of an extension.

Definition 9

(Generating Set). Let ${\Theta }$ be a default theory and ; we call $\varDelta$ a generating set iff there is a total ordering $\lessdot$ on s.t. $\varDelta = \mathsf {D}^{\scriptscriptstyle \lessdot }_{\scriptscriptstyle {\Theta }}(n)$ for , and $\mathsf {D}^{\scriptscriptstyle {\lessdot }}_{\scriptscriptstyle {\Theta }}$ is defined as:

Definition 10

(Extension). Let ${\Theta }$ be a default theory, we say that $E \subseteq \mathscr {F}$ is an extension of ${\Theta }$ iff where is a generating set.

Intuitively, we can think of an extension of a default theory ${\Theta }$ as a set of formulas which contains and which is closed under detachment. We are now in a position to define our default logic.

Definition 11

The default logic $\mathscr {D}\mathsf {IPL}$ is the 3-tuple where: (i) $\mathscr {F}$ is the set of all formulas of $\mathsf {IPL}$; (ii) is the consequence relation of $\mathsf {IPL}$; and (iii) ${\mathscr {E}: {(2^{\mathscr {F}} \times 2^{\mathscr {D}}) \rightarrow 2^{(2^{\mathscr {F}})}}}$ is a function which maps every default theory ${\Theta }$ to its set of extensions, i.e., $E \in \mathscr {E}({\Theta })$ iff E is an extension of ${\Theta }$ (see Definition 10).

The notion of consequence for $\mathscr {D}\mathsf {IPL}$ is introduced below.

Definition 12

(Default Consequence). We say that a formula $\varphi$ is a default consequence of a default theory ${\Theta }$, notation , iff for all $E \in \mathscr {E}({\Theta })$, ².

Some Comments and Easily Established Properties of $\mathscr {D}\mathsf {IPL}$. Definition 10 corresponds to extensions as defined by Łukaszewicz in [27]. This definition of extensions is better behaved than Reiter’s original proposal [37]. In particular, it guarantees existence, i.e., for any default theory ${\Theta }$, $\mathscr {E}({\Theta }) \ne \emptyset$. Definition 10 also guarantees semi-monotonicity. For default theories ${\Theta }_1$ and ${\Theta }_2$, define ${{\Theta }_1 \sqsubseteq {\Theta }_2}$ iff ${\varPhi _{{\Theta }_1} \subseteq \varPhi _{{\Theta }_2}}$ and . Semi-monotonicity implies that for any two default theories ${{\Theta }_1 \sqsubseteq {\Theta }_2}$, if ${\varPhi _{{\Theta }_1} = \varPhi _{{\Theta }_2}}$, then for all ${E_1 \in \mathscr {E}({\Theta }_1)}$, there is ${E_2 \in \mathscr {E}({\Theta }_2)}$ s.t. ${E_1 \subseteq E_2}$. As we will see in Sect. 3, semi-monotonicity is important because it allows us to define a tableaux calculus for default consequence that can take advantage of a partial use of default theories. $\mathscr {D}\mathsf {IPL}$ is non-monotonic; in the sense that there are default theories ${\Theta }_1$ and ${\Theta }_2$ s.t. ${\Theta }_1 \sqsubseteq {\Theta }_2$, , and .

We conclude this section with an example illustrating some of the features and technical elements of $\mathscr {D}\mathsf {IPL}$. The following terminology and notation is useful. A default is normal iff $\rho = \chi$. Normal defaults are written . Let ${\Theta }_1 = (\varPhi _1, \varDelta _1)$ and ${\Theta }_2 = (\varPhi _2, \varDelta _2)$, define ${{\Theta }_1 \sqcup {\Theta }_2} = ({\varPhi _1 \cup \varPhi _2}, {\varDelta _1 \cup \varDelta _2})$. If ${\Theta }_1$ is a default theory, $\varPhi$ a set of formulas, and $\varDelta$ a set of defaults, we use ${\Theta }_1 \sqcup \varPhi$ to mean ${\Theta }\sqcup (\varPhi ,\emptyset )$, and ${\Theta }\sqcup \varDelta$ to mean ${\Theta }\sqcup (\emptyset , \varDelta )$.

Example 1

(Presumption of Innocence). Consider the following propositions:

(1) ‘accused’. (2) ‘guilty or not guilty’. (3) ‘guilty implies not innocent’. (4) ‘the affidavit of a credible witness, the murder weapon, and the results of forensic tests, imply sufficient evidence’. (5) ‘sufficient evidence implies a verdict of guilty’.

In $\mathsf {IPL}$, we would typically formalize (1) to (5) as:

In turn, consider the principle of presumption of innocence, i.e., ‘an accused of committing a crime is a priori innocent’; because of its defeasible status, we choose to formalize it as the (normal) default (6’) .

Let ; then:

Intuitively, the default theory ${\Theta }$ captures the basic set of assumptions discussed in the example in Sect. 1. These assumptions include the possible outcomes of the trial, i.e., the verdict of guilty or not guilty, i.e., $g \vee \lnot g$; the consideration that guilty implies not innocent, i.e., $g \supset \lnot i$; what constitutes sufficient evidence, i.e., $(c \wedge w \wedge f) \supset e$; and the claim that sufficient evidence leads to a verdict of guilty, i.e., $e \supset g$. Each of these assumptions is a default consequence of ${\Theta }$. ${\Theta }\sqcup \{a\}$ considers the particular situation at the beginning of a trial, i.e., someone is accused of committing a crime. It follows that a and i are default consequences of ${\Theta }\sqcup \{a\}$; i.e., if the only thing we know is that someone is accused of committing a crime, we must conclude that said person is innocent, as per the principle of presumption of innocence. In turn, ${\Theta }\sqcup \{a,c,w,f\}$ captures the idea that if we acquire sufficient evidence, in the form of a credible witness affidavit, the murder weapon, and the results of forensic tests, we obtain a verdict of guilt, and in such a situation the principle of presumption of innocence no longer holds (i.e., no longer can be used as a basis for establishing the innocence of the accused).

3 Tableaux Proof Calculus

We develop a tableaux proof calculus for $\mathscr {D}\mathsf {IPL}$ based on one for $\mathsf {IPL}$. The calculus captures default consequence in $\mathscr {D}\mathsf {IPL}$ and it is sound, complete, and terminating (using loop-checks).

Intuitionistic Tableaux. We begin by recalling the basics of a tableaux calculus for $\mathsf {IPL}$. We follow closely the style of presentation of [35].

A tableau is a tree whose nodes are of two different kinds. The first kind corresponds to a pair of a formula $\varphi$ and a natural number i, called a label, appearing in positive form, notation $@^+_{i} \varphi$, or negative form, notation $@^-_{i} \varphi$³. The second kind corresponds to a pair of labels $i$ and $j$, notation $({i},{j})$. Intuitively, $@^+_{i}\varphi$ means “$\varphi$ holds at world i”; and $@^-_{i}\varphi$ means “$\varphi$ does not hold at world i”⁴. Intuitively, $({i},{j})$ means that world j is accessible from world i.

A tableau for $\varphi$ is a tableau having $@^-_{0}\varphi$ as its root. A tableau for $\varphi$ is well-formed if it is constructed according to the expansion rules in Fig. 1. In this figure, ($\wedge ^+$), ($\wedge ^-$), ($\vee ^+$) and ($\vee ^-$), are rules for the logical connectives of conjunction and disjunction. The “positive rules” ($\supset ^+$) and ($\lnot ^+$) for the logical connectives of implication and negation are applied for every j in the branch, whereas the “negative rules” ($\supset ^-$) and ($\lnot ^-$) for these logical connectives create a “new” label j. The latter implies that the positive rules might need to be re-applied, e.g., if a new $({i},{j})$ is introduced in the branch. The rules (ref) and (trans) correspond to the reflexivity and transitivity constraints for the accessibility relation. The rule (her) corresponds to the heredity condition in Kripke models, propagating the valuation of a positive proposition symbol from a world to all its successors. The rule (A) occupies a special place in the construction of a tableau and will be discussed immediately below. Rules are applied as usual: premisses must belong to the branch; side conditions must be met (if any); the branch is extended at the level of leaves according to the consequents.

Fig. 1.

Tableau rules for $\mathsf {IPL}$

Definition 13

(Closedness and Saturation). A branch is closed, tagged $(\blacktriangle )$, if $@^+_{i}\varphi$ and $@^-_{i}\varphi$ occur in the branch; otherwise it is open, tagged $(\blacktriangledown )$. A branch is saturated, tagged $(\blacklozenge )$, if the application of any expansion rule is redundant.

Definition 14

(Provability). A tableau $\tau$ for $\varphi$ is an attempt at proving $\varphi$. We call $\tau$ a proof of $\varphi$ if all branches in $\tau$ are closed. We write if there is a proof of $\varphi$.

Definition 13 introduces standard conditions of closedness and saturation for a tableau. Given these conditions, we define a tableau proof in Definition 14. The resulting proof calculus is sound and complete, i.e., iff (see [35]). Termination is ensured using loop-checks. Loop-checks are a standard termination technique in tableaux systems that require the re-application of expansion rules [17, 23].

Tableaux constructed without the rule (A) formulate a proof calculus for provability, i.e., proofs without assumptions. Including the rule (A) in the construction of a tableau gives us a proof calculus for deducibility (proofs from a set $\varPhi$ of assumptions). Intuitively, (A) can be understood as stating that assumptions are always true in the “current” world. This rule is not strictly necessary: iff , for $\varPhi$ finite. Nonetheless, incorporating a primitive rule for assumptions simplifies the definitions and understanding of tableaux for $\mathscr {D}\mathsf {IPL}$. When (A) is involved, we talk about a tableau for $\varphi$ from $\varPhi$. Such a tableau is well-formed if: its root is $@^-_{0}\varphi$; the rules in Fig. 1 are applied as usual; and (A) is applied w.r.t. the formulas in $\varPhi$. The precise definition of the proof calculus for deducibility is given in Definition 15. By adapting the argument presented in [35], it is possible to prove that the calculus for deducibility is also sound and complete, i.e., iff . Termination is also guaranteed with loop-checks.

Definition 15

(Deducibility). A tableau $\tau$ for $\varphi$ from $\varPhi$ is an attempt at proving that $\varphi$ follows from $\varPhi$. We call $\tau$ a proof of $\varphi$ from $\varPhi$ if all branches in $\tau$ are closed. We write if there is a proof of $\varphi$ from $\varPhi$.

An interesting feature of the tableaux calculus of Definition 15 is that not only it allows us to find proofs, but also lack of proofs. The latter is done by inspecting particular proof attempts, i.e., tableaux having a branch that is both open and saturated. These tableaux serve as counter-examples (i.e., they result in a description of a model which satisfies the assumptions but invalidates the formula we are trying to prove). This claim is made precise in Prop. 1. We resort to this feature as a way of checking consistency of a set of formulas. This check will be used in the definition of an expansion rule for tableaux for $\mathscr {D}\mathsf {IPL}$.

Proposition 1

If a tableau for $\varphi$ from $\varPhi$ has an open and saturated branch, then, .

Corollary 1

iff .

Summing up, Definition 15 characterizes proof theoretically, via tableaux, the semantically defined notion of logical consequence in Definition 4. We repeat that termination of the proof calculus is not ensured by a simple exhaustive application of rules, and loop-checks are required. Intuitively, a loop-check restricts the application of an expansion rule ensuring that only “genuinely new worlds” are created. This technique, traced back to [17, 23], is nowadays standard in tableaux systems.

Default Tableaux. Default tableaux extend tableaux for $\mathsf {IPL}$ with the addition of a new kind of node corresponding to the use of defaults. More precisely, a default tableau is a tree whose nodes are as in tableaux for $\mathsf {IPL}$, together with a third kind that corresponds to the use of a default . By a default tableau for $\varphi$ from ${\Theta }$, where $\varphi$ is a formula and ${\Theta }$ is a default theory, we mean a default tableau having $@^{-}_0 \varphi$ at its root. Such a default tableau is well-formed if it is constructed according to the expansion rules in Figs. 1 and 2. Rules in Fig. 1 are applied as before, with rule (A) being applied w.r.t. formulas in . Rule (D) in Fig. 2 is applied w.r.t. the defaults in . Note that rule (D) is applicable only if its side condition is met. This side condition can be syntactically decided using auxiliary tableaux in $\mathsf {IPL}$ to verify detachment, i.e., to prove that a default is triggered and not blocked.

Fig. 2.

Tableau rule for defaults

Definition 16

(Default Deducibility). Any well-formed default tableau $\tau$ for $\varphi$ from ${\Theta }$ is an attempt at proving that $\varphi$ follows from ${\Theta }$ by default. We call $\tau$ a default proof of $\varphi$ from ${\Theta }$ if all branches of $\tau$ are closed. We write if there is a default proof of $\varphi$ from ${\Theta }$.

The proof calculus just introduced is sound and complete. Termination is guaranteed by the termination of tableaux for $\mathsf {IPL}$. Figure 3 shows a default proof.

Fig. 3.

Default tableau for $u_1 \wedge u_2$ from .

Theorem 1

iff . Since terminates, also terminates.

Proof

(Sketch). We make use of the already known soundness and completeness of deducibility of the tableaux calculus for $\mathsf {IPL}$. The proof of soundness and completeness of default deducibility depends on the following two observations: (i) a branch of a default tableau contains a branch of a tableau for deducibility in $\mathsf {IPL}$ (just remove default nodes); and (ii) defaults appearing in an open and saturated branch of a default tableau define a generating set (as per Definition 9) by construction. (i) and (ii) implies that if there is an open and saturated branch of a default tableau, then, there is an extension which serves as a counter-example. This proves that if , then . For the converse, suppose that ; hence there is an extension $E \in \mathscr {E}({\Theta })$ s.t. . Let $\tau$ be any saturated default tableau for $\varphi$ from ${\Theta }$; by construction, there is an open branch of $\tau$ which contains a set of defaults which is a generating set for E. The result follows from the completeness of deducibility for $\mathsf {IPL}$.

4 Implementation

Overview. DefTab is an implementation of the default tableau calculus presented in Sect. 3. It is available at http://tinyurl.com/deftab0.

Given ${\Theta }$ and $\varphi$ as input, DefTab builds proof attempts of by searching for Kripke models for $\varphi$, and subsequently restricting these models with the use of sentences from and defaults from . DefTab reports whether or not a default proof has been found. In the latter case, DefTab exhibits an extension of ${\Theta }$ from which $\varphi$ does not follow.

Defaults Detachment Rule and Sub-tableaux. The following is a brief explanation of how defaults are dealt with in DefTab. At any given moment, DefTab maintains defaults in three lists: available, triggered, and detached. The available list contains the defaults of the input default theory. An available default is triggered if $\pi$ is deduced from the set of the default theory ${\Theta }$ under question, together with the consequents of the defaults already in the branch of the tableau. Once triggered, available defaults are moved to the list of triggered defaults. DefTab uses the latter list to apply rule (D) in Fig. 2 and generates a (temporary) sub-list of non-blocked defaults. This sub-list of non-blocked defaults corresponds to the branching part of rule (D). DefTab then takes defaults from the sub-list of non-blocked defaults and moves them from the triggered list to the detached list, expanding the default tableau accordingly. Since the application of rule (D) requires checking consequence and consistency in $\mathsf {IPL}$, for each (D)-step, DefTab builds a corresponding number of intuitionistic tableaux.

Blocking and Optimizations. For loop-checking intuitionistic rules that create new labels, DefTab uses a blocking technique called pattern-based blocking [25], initially designed for modal logics. In the present tableau system, when rule $(\lnot ^-)$ can be applied to some formula $@^-_i \lnot \varphi$, it is first checked that no label k exists such that the set of formulas $\{@^-_k \varphi \} \cup @_k C(i)$ hold, where C(i) are the constraints that formulas at label i forces on all its successors. If such a label exists, then the rule is not applied. The same occurs for rule $(\supset ^-)$.

DefTab does not include semantic branching, or any other optimization based on Boolean negation and the excluded middle (which are usually unsound in an intuitionistic setup). Backjumping [24], on the other hand, is intuitionistically sound, and preliminary testing shows that it greatly improves performance.

We take special care of tracking dependencies of the consequent formulas introduced by the application of rule (D). That is, once a default is triggered, we bookkeep it along with the set of formulas that triggered it. Concretely, this bookkeeping is the union of the dependencies of all defaults $\varDelta$ s.t. . Note that this set can overestimate the set of dependencies of the triggered rule. This is a trade-off between being precise and limiting the number of sub-tableaux runs.

Usage. DefTab takes as input a file indicating the underlying logic to be used, a default theory partitioned into its set of formulas and set of defaults, and the formula to be checked. The structure of this input file is illustrated in the following example file presumption.dt. This file corresponds to Example 1 where: $g \mapsto \mathtt {P1}$, $i \mapsto \mathtt {P2}$, $a \mapsto \mathtt {P3}$, $c \mapsto \mathtt {P4}$, $w \mapsto \mathtt {P5}$, $f \mapsto \mathtt {P6}$, $e \mapsto \mathtt {P7}$.

DefTab is executed from the command line as

The output indicates that P2 is a sceptical consequence of the default theory. If we add the facts P4; P5; P6;, we obtain that P2 is not a sceptical consequence, indicated by the output: Not a sceptical consequence, found bad extension: []. The list [] indicates the defaults in the extension, in this case none. DefTab includes in the output a counter-example for disproving the candidate default consequence. Such counter-example consists of the generator set of the corresponding extension. In this case, the empty list indicates that the set of facts itself (without any default) is enough to generate the extension.

5 Preliminary Testing

To our knowledge, there is no standard test set for automated reasoning for default logic, and less so (if possible) for default reasoning based on IL. Moreover, our tool is a first prototype which still needs the implementation of many natural optimizations (e.g., catching for sub-tableaux results). Hence, any empirical testing is, by force, very preliminary, and should be taken only as a first evaluation of the initial performance of the tool, and of its current usability. Still, the results are encouraging and the prover seems to be able to handle examples which are well beyond what can be computed by hand, making it already a useful tool. We discuss below the tests sets we evaluated. All tests were performed on a machine running Ubuntu 16.04 LTS, with 8 GB of memory and an Intel Core i7-5500U CPU @ 2.40 Ghz.

Purely Intuitionistic Problems. When no defaults are specified in the input file, DefTab behaves as a prover for consequence in $\mathsf {IPL}$ (but it has not particular optimization for the case where the input is just an intuitionistic formula). Even though DefTab is still a prototype, we carried out a comparison of its performance w.r.t. existing provers for $\mathsf {IPL}$.

We extend the comparison of provers for $\mathsf {IPL}$ carried out in [11] which compares their own prover (intuit) that implements satisfiability checking in $\mathsf {IPL}$ by an SMT (Satisfiability Modulo Theories) reasoner implemented over MiniSAT [13], with IntHistGC [21] and fCube [16]. These two last provers perform a backtracking search directly on a proof calculus, and are rather different from the approach taken by intuit, and closer to DefTab. IntHistGC implements clever backtracking optimizations that avoid recomputations in many cases. fCube implements several pruning techniques on a tableau-based calculus. Tests are drawn from three different benchmark suites.

• 1. ILTP [36] includes 12 problems parameterized by size. The original benchmark is limited, and hence it was extended as follows: two problems were generated up to size 38 and all other problems up to size 100, leading up to a total of 555 problem instances.

• 2. Benchmarks crafted by IntHistGC developers. These are 6 parameterized problems. They are carefully constructed sequences of formulas that separate classical and intuitionistic logic. The total number of instances is 610.

• 3. API solving; these are 10 problems where a rather large API (set of functions with types) is given, and the problem is to construct a new function of a given type. Each problem has variants with API sizes that vary in size from a dozen to a few thousand functions. These problems were constructed by the developers of intuit in an attempt to create practically useful problems. The total number of instances is 35.

Fig. 4.

Comparison on $\mathsf {IPL}$: fCube, intuit, IntHistGC.

Figure 4 shows a scatterplot (logscale) of the performance of DefTab with the other three provers, discriminating between valid and not valid formulas. Times shown are in seconds, and the timeout was set to 300 seconds. Point below the diagonal show cases where DefTab performance is worse that the other provers. The empirical tests show that specialized provers for $\mathsf {IPL}$ (and in particular intuit) outperforms DefTab, specially on valid, complex formulas. On simple, not valid formulas, the performance of DefTab in this test is better than fCube and comparable to IntHistGC.

Broken Arms [34]. Consider an assembly line with two mechanical arms. We assume that an arm is usable ($u_i$), but sometimes it can be broken ($b_i$), although a broken arm is an exception. In the literature on Default Logic such default assumptions have been formalized either as:

$\varDelta _1$ can be found in Poole’s original discussion of the example (see [34]), whereas $\varDelta _2$ is found in, e.g., [1, 14]. Suppose that we know as a fact that one of the arms is broken, but we do not know which one, i.e., $b_1 \vee b_2$. Let and ; it is possible to prove that and that . Poole introduces this example to argue that having $u_1 \wedge u_2$ as a default consequence of ${\Theta }_1$ is counter-intuitive; as we have as a fact that one of the arms is broken. This counter-intuitive result has inspired some important work on Default Logic [6, 12, 29]. Here, we choose this example, and ${\Theta }_1$ in particular, merely as a test case. First, observe that ${\Theta }_1$ can easily be made parametric on the number of arms (the number of defaults grows linearly with the number of arms). Second, observe that since defaults do not block each other, they can all be detached at any given time in a default proof attempt. The latter means that the prover needs, a priori, to consider a large number of combinations, leading to a potentially large search space. On the other hand, the intuitionistic reasoning needed is controlled, and as a result, the test case should mostly highlight how default are handled by the prover. These observations make this example a good candidate for testing the implementation of our proof calculus in order to evaluate its performance in a small, but non-trivial case. The results of running DefTab with n defaults are reported below.

No. of defaults	10	20	40	60	80
run time	0.038 s	0.499 s	8.667 s	49.748 s	177.204 s

Abstract. The following example, actually, an example template, is a variation of Broken Arms, where defaults do not block one another, but in which the detachment of defaults involves “non-trivial” intuitionistic formulas. This example is built on the ILTP library. To provide a bit of context, the ILTP library has two kinds of problems: those testing consequence in $\mathsf {IPL}$, i.e., problems ; and those testing not-consequence in $\mathsf {IPL}$, i.e., problems . Of the problems testing not-consequence, we are interested in a particular sub-class, i.e., those of the form . Problems in this sub-class can directly be used for testing blocking of defaults. Now, for each pair and , we construct a default theory . We carry out this construction guaranteeing that the languages of ${\varPhi _i \cup \varphi _i}$ are disjoint via renaming of proposition symbols and that p is new. Then, we consider a family of default theories constructed in the way just described. It can be proven that . This construction serves as a way to test our implementation on increasingly more difficult default theories built on the ILTP library. The next table reports the results of running DefTab on where:

${{}_{n} \backslash }^{m}$	1	2	3	4	5
1	2.20e−3 s	1.50e−2 s	0.15 s	1.15 s	11.29 s
2	1.99e−3 s	2.23e−2 s	0.25 s	2.17 s	17.17 s
3	2.8e−3 s	3.7e−2 s	0.39 s	3.29 s	26.08 s

Intuitively, ${\Theta }_n^m$ contains m instances of sub-problems and of size n taken from the ILTP. The sub-indices in $\varPhi _m^n$ and $\varGamma _m^n$ ensure languages are disjoint. It follows that every default is detached by ${\varPhi _i^n \cup \varGamma _i^n}$; and also that no default blocks any other. Thus, . The times show the progression of running DefTab on increasingly larger default theories ${\Theta }_n^m$. Note the increase on complexity is both on m and n.

6 Final Remarks

We introduced $\mathscr {D}\mathsf {IPL}$, a Default Logic to reason non-monotonically over Propositional Intuitionistic Logic. This logic is motivated by Normative Systems and Legal Artificial Intelligence in order to deal, e.g., with legal conflicts due to logical inconsistencies. Our contribution is twofold. First, we present a sound, complete and terminating tableaux calculus for $\mathscr {D}\mathsf {IPL}$, which decides if a formula $\varphi$ is a logical consequence of a default theory ${\Theta }$. The calculus is based on tableaux for $\mathsf {IPL}$ as presented in [35], combined with the treatment for defaults of [7]. Second, we provide a prototype implementation for our calculus in the DefTab prover.

To the best of our knowledge, this is the first prover combining Intuitionistic Logic with Non-monotonic Reasoning. For instance, DeReS [10] is a default logic reasoner with an underlying propositional tableaux calculus. It is designed to check logical consequence by combining defaults reasoning and the underlying logic reasoning as ‘black boxes’. This contrasts with DefTab which integrates these two reasonings in a same tableaux calculus. On the other hand DefTab only supports sceptical consequence checking, while DeReS also supports credulous consequence checking. In [15], a tableaux calculus for Intuitionistic Propositional Logic is presented, with a special treatment for nested implications. The implementation is no longer available, but it would be interesting to implement their specialized rules in DefTab. More directly related to our work are [1], where the authors present a sequent calculus for a Non-monotonic Intuitionistic Logic; and [14], where a tableaux method is presented but only for the computation of extensions, and with no implementation.

We ran an empirical evaluation of our prover and obtained preliminary results concerning the implementation. To test purely intuitionistic reasoning we used the ILTP problem library [36]. We tested non-monotonic features in two, very small, case examples (broken arms and abstract). Clearly further testing is necessary. In particular, we are interested in crafting examples that combine the complexities of non-monotonic and intuitionistic reasoning.

For future work there are several interesting lines of research. As we mentioned, the treatment of defaults in the calculus is almost independent from the underlying logic. As a consequence, it would be interesting to define a calculus which is parametric on the rules for the underlying logic (see, e.g., [8] for such a proposal). We believe that (modulo some refactoring in the current source code) the implementation of DefTab can be generalized to handle defaults over different underlying logics obtaining a prover for a wide family of Default Logics.