Representational change is integral to reasoning

(a) Cauchy’s ‘proof’ and some counterexamples to it

Lakatos’ book starts with a ‘proof’, due to Cauchy, illustrated by figure 1.

• Download figure
• Open in new tab
• Download PowerPoint

We have put scare quotes around ‘proof’ because Cauchy’s ‘Proof’ is no more a proof than Euler’s ‘Theorem’ is a theorem. It is claimed that this same procedure can be carried out on any polyhedron. But this claim has been shown to be false. Lakatos’ students soon come up with counterexamples. Two of these are depicted in figure 2.

• Download figure
• Open in new tab
• Download PowerPoint

(b) The changing definition of polyhedron

The students, however, are able to rescue these counterexamples and turn them into examples. They did this by choosing an appropriate definition of polyhedron or polygon. In the case of the hollow cube, they contrasted a solid structure with a plate structure.

Solid structure:	A polyhedron is a solid whose surface consists of polygonal faces.
Plate structure:	A polyhedron is a surface consisting of a system of polygons.

In the case of the plate structure, the hollow cube becomes one cube nested within another. For each one $V-E+F=2$.

Intersecting edges:	A polygon is a system of edges arranged in such a way that exactly two edges meet at each vertex.
Non-intersecting edges:	A polygon is a system of edges arranged in such a way that exactly two edges meet at each vertex and the edges have no points in common except the vertices.

The second definition excludes edges that intersect, so the pentagram is ruled out as a polygon. If, on the other hand, we interpret the triangles as the faces, then there are 32 of them, with 90 edges and 60 vertices, so $V-E+F=60-90+32=2$.

Lakatos calls this tactic of rejecting a counterexample via a change of definition, monster barring.

Now we are confronted by a conundrum:

The answer is that both were generalizing from a finite set of examples. They knew about the five Platonic solids of a tetrahedron, cube, octahedron, dodecahedron, icosahedron and a few more. Euler’s conjecture and Cauchy’s proof both worked for them. There were others, however, for which whether it worked or not depended on definitions that they had not formulated.

We claim that this state of affairs is commonplace. Despite it imposing a strict discipline of formal definitions, representational change can even arise in modern mathematics. For instance, Robinson’s non-standard analysis [2] has extended the concept of ‘number’ to include infinite and infinitesimal numbers, and intuitionistic logic has divided the concept of ‘proof’ into ‘classical’ and ‘constructive’.

Reasoning based only on examples is a frequent cause of computer failures. A program may run successfully on a finite set of test examples then, but later encounter so-called, ‘edge cases’, on which they fail.

Formal verification of computer programs can avoid this problem because it proves the correctness of the program for the, potentially infinite, set of all cases. It requires, though, a formal logical definition of all cases and this is still error prone since it is a non-trivial task to formulate such a definition.

This motivated us to attempt to automate the repair of faulty logical theories. This is not just a matter of enlarging or reducing the axioms of a theory. It also entails refining the language in which they are expressed. We saw such language refinement in the case of polyhedra in the debate over whether they were solid or plate structured and over whether a polygon’s edges could intersect. In this spirit, we developed the ABC theory repair system [3,4].

(a) Datalog theories

Datalog is a logic programming language consisting of Horn clauses in which there are no functions except constants [6]. We use this notation to define a subset of first-order logic that we also call Datalog. We choose Datalog because it is decidable under SL and ABC requires¹ decidability in the detection of faults. We represent formulae in Datalog as clauses in Kowalski normal form, shown in definition 2.1 below.

Definition 2.1. (Datalog formulae)

Let the language of a Datalog theory $\mathbb{T}$ be a triple $⟨\mathcal{P},\mathcal{C},\mathcal{V}⟩$, where $\mathcal{P}$ are the propositions, $\mathcal{C}$ are the constants and $\mathcal{V}$ are the variables. We will adopt the convention that variables are written in lower case, and constants and predicates start with a capital letter.²

A proposition is a formula of the form $P(t_1,\dots ,t_n)$, where $t_j\in \mathcal{C}\cup \mathcal{V}$ for $1\le j\le n$, i.e. there are no compound terms. Let $R\in \mathcal{P}$ and $Q_i\in \mathcal{P}$ for $0\le i\le m$ in $\mathbb{T}$. Datalog clauses are of the four types in definition 2.2, $R$ is called the head of the clause and the conjunction of the $Q_i$s forms the body.

Definition 2.2.

Kowalski Form Horn clauses

Implication:	$(Q_1\wedge \dots \wedge Q_m)\hspace{0.17em}⟹\hspace{0.17em}R$, where $m>0$. These usually represent the rules of $\mathbb{T}$.
Assertion:	$\hspace{0.17em}⟹\hspace{0.17em}R$, i.e. the body is empty. When $R$ contains no variables the assertion is called ground. These ground assertions represent the facts of $\mathbb{T}$ and the members of $\mathcal{T}(\mathbb{P}\mathbb{S})$ and $\mathcal{F}(\mathbb{P}\mathbb{S})$.
Goals:	$Q_1\wedge \dots \wedge Q_m\hspace{0.17em}⟹\hspace{0.17em}$, i.e. the head is empty. These usually arise from the negation of the conjecture to be proved and from subsequent subgoals in a derivation.
Empty Clause:	$\hspace{0.17em}⟹\hspace{0.17em}$, i.e. both the head and body are empty. This represents false, which is the target of a reductio ad absurdum proof. Deriving it, therefore, represents success in proving a conjecture.

(b) Selected literal resolution

SL is a complete, reductio ad absurdum proof procedure for first-order logic expressed in clausal form [5]. When restricted to Datalog clauses, such as those defined in definition 2.2, SL is a decision procedure. This means that ABC can decide whether a given conjecture is or is not a theorem of a Datalog theory $\mathbb{T}$.

Definition 2.3. (A deductive step in SL)

A deductive step in SL is between a goal clause and either an assertion or a rule, which we will collectively call an axiom. A proposition in the goal clause and the head of the axiom must unify, that is it must be possible to instantiate each of them so that they are identical. An instantiation $\sigma$ replaces variables by constants. We write $\varphi \sigma$ to mean that proposition $\varphi$ is instantiated by substitution $\sigma$. The substitution used in an SL step is called a most general unifier [8]. We will depict such an SL step as

where $\sigma$ is the most general unifier of $Q_i$ and $R$.

Definition 2.4. (An SL refutation)

Because a proof in SL is by reductio ad absurdum, we call it a refutation. It consists of a series of SL steps. Each step takes as input the goal clauses produced by the previous step and outputs the goal clauses to be used in the next step. In the final step, one goal proposition remains and an assertion is unified with it to leave the empty goal clause $\hspace{0.17em}⟹\hspace{0.17em}$. We can depict such a refutation as follows:

If an SL refutation proves a formula $\varphi$ using the axioms from theory $\mathbb{T}$. We write $\mathbb{T}⊢\varphi$.

(c) Types of fault

Given a preferred structure $\mathbb{P}\mathbb{S}$, a theory $\mathbb{T}$ could have two kinds of faults:

Incompatibility:	Predictions that arise from the agent’s representation conflict with observations of their environment: $\mathrm{\exists }\varphi .\hspace{0.17em}\mathbb{T}⊢\varphi \wedge \varphi \in \mathcal{F}(\mathbb{P}\mathbb{S})$.
Insufficiency:	The agent fails to predict observations of its environment: $\mathrm{\exists }\varphi .\hspace{0.17em}\mathbb{T}⊬\varphi \wedge \varphi \in \mathcal{T}(\mathbb{P}\mathbb{S})$.

Since SL is decidable for Datalog theories [9], ABC can exhaustively test all members of both $\mathcal{T}(\mathbb{P}\mathbb{S})$ and $\mathcal{F}(\mathbb{P}\mathbb{S})$ for theorem-hood. So it can detect all occurrences of insufficiency and incompatibility in a Datalog theory.

(d) ABC repair operations

An insufficiency may be repaired by unblocking a proof with additional necessary SL steps, while an incompatibility may be repaired by blocking all its proofs, which can be done by breaking one SL step in each of them [3]. ABC repairs faulty theories using 11 repair operations. There are five for repairing incompatibilities and six for repairing insufficiencies. These are defined in definitions 2.5 and 2.6.

Definition 2.5. (Repair operations for incompatibility)

In the case of incompatibility, the unwanted proof can be blocked by causing any of the SL steps to fail. Suppose the targeted SL step is between a goal, $P(s_1,\dots ,s_n)$, and an axiom, $Body\hspace{0.17em}⟹\hspace{0.17em}P(t_1,\dots ,t_n)$, where each $s_i$ and $t_i$ pair can be unified. Possible repair operations are as follows:

Belief Revision 1:	Delete the targeted axiom: $Body\hspace{0.17em}⟹\hspace{0.17em}P(t_1,\dots ,t_n)$.
Belief Revision 2:	Add an additional precondition to the body of an earlier rule axiom which will become an unprovable subgoal in the unwanted proof.
Reformation 1c:	Rename $P$ in the targeted axiom to either a new predicate or a different existing predicate $P^{\prime }$.
Reformation 2c:	Increase the arity of all occurrences $P$ in the axioms by adding a new argument. Ensure that the new arguments in the targeted occurrence of $P$, are not unifiable. In Datalog, this can only be ensured if they are unequal constants at the point of unification.
Reformation 3c:	For some $i$, suppose $s_i$ is $C$. Since $s_i$ and $t_i$ unify, $t_i$ is either $C$ or a variable. Change $t_i$ to either a new constant or a different existing constant $C^{\prime }$.

Definition 2.6. (Repair operations for insufficiency)

In the case of insufficiency, the wanted but failed proof can be unblocked by causing a currently failing SL step to succeed. Suppose the chosen SL step is between a goal $P(s_1,\dots ,s_m)$ and an axiom $Body\hspace{0.17em}⟹\hspace{0.17em}{P}^{\prime }(t_1,\dots ,t_n)$, where either $P\ne P^{\prime }\hspace{0.17em}\mathrm{or}\hspace{0.17em}m\ne n$ or for some $i$, $s_i$ and $t_i$ cannot be unified. Possible repair operations are

• Abduction 1: Add the goal $P(s_1,\dots ,s_m)$ as a new assertion and replace variables with constants.

• Abduction 2: Add a new rule whose head unifies with the goal $P(s_1,\dots ,s_m)$ by analogizing an existing rule or formalizing a precondition based on a theorem whose arguments overlap with the ones of that goal.

• Abduction 3: Locate the rule axiom whose precondition created this goal and delete this precondition from the rule.

• Reformation 1s: Replace $P^{\prime }(t_1,\dots ,t_n)$ in the axiom with $P(s_1,\dots ,s_m)$.

• Reformation 2s: Suppose $m=n$ but $s_i$ and $t_i$ are not unifiable. Decrease the arity of all occurrences $P^{\prime }$ by 1 by deleting its $i$th argument.

• Reformation 3s: If $m=n$ but $s_i$ and $t_i$ are not unifiable, then they are unequal constants, say, $C$ and $C^{\prime }$. Either (i) rename all occurrences of $C^{\prime }$ in the axioms to $C$ or (ii) replace the offending occurrence of $C^{\prime }$ in the targeted axiom by a new variable.

Belief Revision 1 is inherited from Gärdenfors [10]. Belief Revision 2 extends this by adding a precondition that will create a subgoal that will be unprovable in the unwanted proof. Similarly, Abduction 1 is inherited from Cox & Pietrzykowski [11] and Abduction 2 extends this by removing a precondition that has given rise to an unprovable subgoal. The various Reformation operations are adapted from Bundy & Mitrovic [7]. They break new ground by evolving the language of the faulty theory, e.g. by creating new predicates and constants. In [7], the different forms of Reformation arose by an exhaustive analysis of ways in which the first-order unification algorithm [8] could defeat or enable the matching of a goal to an axiom in an unwanted proof or a failed but wanted proof, respectively.

We are not claiming that these 11 repair operations are complete. Indeed, we doubt that a claim of completeness could be made of any set of theory repair operations. Human ingenuity is unbounded and no one could anticipate all possible forms that theory repair could take. Moreover, the forms of theory repair depend on the kind of logic that a theory is expressed in. In a sorted logic, for instance, manipulations of the type hierarchy offer additional opportunities [12]. In an equational logic, different forms of inference are required, but proofs can still be blocked or unblocked at the application of a matching operation [13]. In a probabilistic logic, the assigned probabilities can be changed [14]. Therefore, we can only make empirical claims about the range of applications of the ABC system.

(e) Related work

In §2d, we briefly discussed the relationship of the ABC repair operations to both belief revision [10] and abduction [11]. There is also a tradition of theory revision in Inductive Logic Programming. In [15], Shapiro presented an algorithm for debugging logic programs. Given a faulty logic program, it recurses through a failed execution of the program using an oracle to check the truth of each sub-routine call. If one of these is false, this process will eventually identify the root cause of the fault, namely a false clause. This clause can then be replaced. [16,17] subsequently built on this work. For instance, de Raedt’s RUTH system used integrity constraints to provide the oracle and repaired faulty programs by a combination of belief revision and abduction.

These theory revision programs focus on the identification of the faults. The ABC System uses the preferred structure to do this, by trying to prove assertions from both $\mathcal{T}(\mathbb{P}\mathbb{S})$ and $\mathcal{F}(\mathbb{P}\mathbb{S})$. Success in proving an assertion in $\mathcal{F}(\mathbb{P}\mathbb{S})$ constitutes an incompatibility and failure to prove an assertion in $\mathcal{T}(\mathbb{P}\mathbb{S})$ constitutes an insufficiency. ABC’s novelty lies, though, in its repair operations, which go beyond belief revision and abduction, to include reformation. ABC does not just add or delete clauses but changes the language in which they are expressed. Thus systems such as RUTH and ABC are complementary and could be combined.

(a) The optimal maximal set of commutative repairs

Commutative repairs are the ones that can be applied in any order, for instance, because they repair different parts of a theory to solve different faults. Thus, we refine the naive search method so that it computes only maximal sets of commutatives repairs (MSCRs). As the repairs in an MSCR can be applied together, the search space of fault-free theories using MSCR is reduced dramatically.

Not all repairs are commutative.

(i)	It is possible that after applying one repair $r_1$, another repair $r_2$ will not be needed because $r_1$ has also solved the fault which $r_2$ targeted.
(ii)	On the other hand, $r_1$ may make $r_2$ inapplicable. For instance, $r_1$ may merge predicate $mother$ with predicate $mum$. Then, if $r_2$ would have deleted an axiom of $mother$, it cannot find it after $r_1$’s application.

These are the scenarios where repairs are not commutative because applying them in different orders results in different repaired theories.

The commutation between repairs $r_1$ and $r_2$ is defined in definition 3.1. $\mathbb{T}\cdot r$ represents the application of a repair $r$ to a theory $\mathbb{T}$.

Definition 3.1. (Commutative repairs)

Two repairs $r_1$ and $r_2$ are commutative if applying them in different orders to theory $\mathbb{T}$ results in the same repaired theory.

$$\mathbb{T}\cdot r_1\cdot r_2=\mathbb{T}\cdot r_2\cdot r_1.$$3.1

Accordingly, the maximal set of commutative repairs is defined in definition 3.2.

Definition 3.2. (Maximal set of commutative repairs)

Given the whole set of all possible repairs $\mathbb{R}$ for all detected faults in the theory $\mathbb{T}$, an MSCR $\mathbb{M}$ is a maximum set of $\mathbb{T}$’s commutative repairs if they avoid the scenarios illustrated in (i) and (ii). We can formalize this as follows:

$$\mathrm{\exists }{r}_m\in \mathbb{M},\hspace{0.17em}\mathrm{\forall }r\in \mathbb{R}\setminus \mathbb{M},\hspace{0.17em}\mathbb{S}(\mathbb{T},r)\wedge \mathbb{S}(\mathbb{T},r_m)\ne \mathrm{\varnothing }$$3.2

and

$$\mathrm{\forall }{r}_1,r_2\in \mathbb{M},\text{ if }{r}_1\ne r_2,\text{ then }\mathcal{F}(\mathbb{T},\hspace{0.17em}{r}_1)\ne \mathcal{F}(\mathbb{T},\hspace{0.17em}{r}_2),$$3.3

where $\mathbb{S}(\mathbb{T},r)=\{\alpha |\alpha \in \mathbb{T}\wedge \alpha \notin \mathbb{T}\cdot r\}$ is the scope of a repair $r$ in the theory $\mathbb{T}$, and $\mathcal{F}(\mathbb{T},r)$ is the fault in $\mathbb{T}$ that a repair $r$ solves.

There could be $n$ MSCRs, where $n\ge 1$, and a repair can belong to more than one MSCR. ABC computes all MSCRs and applies each MSCR separately to produce $n$ semi-repaired theories, which will be delivered for the next round of fault detection and repair generation. By applying repairs in an MSCR together, the search space is reduced because the search branches of grouped repairs are merged into one. The comparison of search spaces is drawn in figure 4.

Inspired by the sub-optimal pruning of ABC repairs based on Max-Sat [18], an optimal MSCR is defined as follows:

Definition 3.3. (Optimal MSCR)

An MSCR, ${\mathbb{M}}_1$, is optimal for the theory $\mathbb{T}$ if and only its estimated cost $c(\mathbb{T}\hspace{0.17em}\hspace{0.17em}{\mathbb{M}}_1)$ is not bigger than any of the MSCRs of that theory, denoted as ${\mathbb{M}}_2$:

$$\mathrm{\forall }{\mathbb{M}}_2.\hspace{0.17em}c(\mathbb{T},\hspace{0.17em}{\mathbb{M}}_1)\le c(\mathbb{T},\hspace{0.17em}{\mathbb{M}}_2),$$3.4

where the estimated cost is

$$c(\mathbb{T},\hspace{0.17em}\mathbb{M})=|\mathbb{M}|+{\mathcal{N}}_{\text{insuff}}({\mathbb{T}}_m)+{\mathcal{N}}_{\text{incomp}}({\mathbb{T}}_m),$$

where $|\mathbb{M}|$ is the number of repairs in $\mathbb{M}$ and ${\mathcal{N}}_{\text{insuff}}({\mathbb{T}}_m)$ and ${\mathcal{N}}_{\text{incomp}}({\mathbb{T}}_m)$ are the number of insufficiencies and incompatibilities of ${\mathbb{T}}_m$, respectively, and where ${\mathbb{T}}_m$ is the repaired theory produced by applying all repairs in $\mathbb{M}$ to $\mathbb{T}$.

By only taking the optimal MSCRs to the remaining repair process, the search space of fault-free theories is further reduced. This method dramatically saves time and space.

(b) Other ranking mechanisms

Another ranking mechanism is inspired by Gärdenfors epistemic entrenchment [10]. This is defined to represent the informational value of a belief so that it can guide a repair system to change the beliefs of the least informational value while keeping the others untouched. Based on the idea of epistemic entrenchment, the vitality of an axiom or a precondition is defined as scores [19], which rank repaired theories so that the best ones are prioritized at the top. Also, the entrenchment of the theory’s signature³ is explored to rank repairs [20].

Another ranking mechanism is based on probability. In a probabilistic logic, a theory can be assigned an overall probability based on the probabilities assigned to its assertions and implications. A probabilistic version of ABC is described in [14].

In future work, we hope to explore the design of extensions to the preferred structure that might distinguish between alternative repairs. Consider, for instance, the use of ABC to diagnose what misconceptions about arithmetic might be the cause of a student’s errors, which we discuss below in §5e. More than one misconception might explain the observed errors. A teacher might set the student an arithmetic problem that would result in different outcomes depending on which misconception the student was suffering from.

(a) Defeasible reasoning

Defeasible reasoning occurs when a rule is given, but there may be specific exceptions to it. We will call such a rule defeasible. In AI, defeasible reasoning has usually been formalized by some kind of non-monotonic logic [22]. Logical theories are normally⁶ monotonic, i.e. adding extra axioms to a theory increases its set of theorems. In a non-monotonic theory adding a new axiom can sometimes override some applications of a defeasible rule, so that of proofs of some theorems will no longer hold.

We offer an alternative mechanism using only monotonic logical theories, i.e. a monotonic theory containing a faulty rule is repaired into another monotonic theory in which the fault has been eliminated.

The classic example of defeasible reasoning is about $tweety$ the penguin: a non-flying bird. We have formalized both the original faulty theory and its repair in example 5.1.

The left hand theory ${\mathbb{T}}_b$ has an incompatibility fault: ${\mathbb{T}}_b⊢fly(tweety)$ but $fly(tweety)\in \mathcal{F}(\mathbb{P}\mathbb{S})$. The repair operation Reformation 2c is applied to add an additional argument to $bird$ in all occurrences in theory ${\mathbb{T}}_r$ and these are highlighted in red. This argument is given the value $normal$, $abnormal$ or a variable. This prevents the unification of $bird(X,normal)$ with $bird(X,abnormal)$, which is required to prove $fly(tweety)$. The proofs of the members of $\mathcal{T}(\mathbb{P}\mathbb{S})$ are unaffected by this repair.

ABC also finds a repair in which Reformation 1c is used to rename $bird$ in the axiom to a new predicate ${bird}^{\prime }$, representing flying birds, where $bird$ now means non-flying ones. To avoid introducing an insufficiency, the axiom $bird(X)\hspace{0.17em}⟹\hspace{0.17em}feathered(X)$ axiom now has to be duplicated for ${bird}^{\prime }$. This is a disadvantage of Reformation 1c over Reformation 2c in this case.

(b) Modelling virtual bargaining

Virtual Bargaining is a term coined by Cognitive Scientist, Nick Chater, to describe the extraordinary ability to cooperate with humans to reach a, sometimes complex, agreement with only minimal channels of communication. It relies on their ability to put themselves in the shoes of their partner to imagine how they will understand these minimal communications [23].

To illustrate virtual bargaining, Misyak et al. [23] invent a two-person cooperative game called bananas and scorpions. In this game, the human players need to guess or adjust the winning strategy based only on the others’ game moves. The two players are the sender and the receiver. There are three boxes of two kinds: the helpful (containing bananas) and the harmful (containing scorpions). The sender knows all the boxes’ contents and marks one of them to guide the receiver to choose a helpful box by marking only one box. On the other hand, the receiver only knows the number of each type of box, and which box is marked, and then aims to select as many helpful boxes as possible.

Two rounds of the game are illustrated in figure 6. In the first round (g1), only box $b1$ is helpful and boxes $b2$ and $b3$ are harmful while the opposite is true in the second round (g2): $b2$ and $b3$ are helpful and $b1$ is harmful.

• Download figure
• Open in new tab
• Download PowerPoint

Given this limited bandwidth, each player has to imagine what the other is thinking and plan their play. In situation (g1), the sender has marked the only box marked ‘Help’. This is a natural strategy to adopt. It is akin to pointing at the box you want to have opened. But in the situation (g2), the strategy is less obvious. The sender could mark one of the two ‘Help’ boxes, but cannot mark both, as only one tick is allowed. The receiver could then open this box, but this is a sub-optimal outcome, as the best outcome would be to open both ‘Help’ boxes. Bearing this in mind, the sender has changed strategy to mark the single ‘Harm’ box, intending the receiver to open both ‘Help’ boxes. Remarkably, the human players of the game frequently and spontaneously adopted this strategy, thus confirming their ability to do virtual bargaining. They did not first have to experiment to see which strategy was being used.

In [24], our research group modelled this process. Our Datalog theories were logic programs that the sender and receiver would invent and the receiver could then use to select which boxes to open. The starting theory $\mathbb{T}$ contains an insufficiency, which is easily repaired to solve g1. However, it would have failed completely on g2, because it would have opened a harmful box and would have failed to open either of the helpful ones.

The key rule in $\mathbb{T}$ was

which can be interpreted as ‘select the marked box’, where $mark(X,Y)$ means ‘in game $X$ mark box $Y$’ and $select(X,Y)$ means ‘in game $X$ select box $Y$’. The preferred structure was and Using the red and green diamonds, this reflects the receiver’s knowledge of the two games. In $g_1$, $b_{\text{green}}$ stands for whichever box is known to be helpful and $b_{\text{red1}}$ and $b_{\text{red}2}$ the two boxes known to be harmful. In $g_2$, it is $b_{\text{green}1}$ and $b_{\text{green}2}$ that are known to be helpful and $b_{\text{red}}$ that is harmful. Note that we must not assume that the receiver knows which actual boxes these correspond to, e.g. the receiver does not initially know that in $g_1$, $b_{\text{green}}$ will turn out to be $b_1$, the marked box.

The insufficiency in $g_1$ is that $\mathbb{T}⊬select(g_1,b_{\text{green}})$. The proof fails because $mark(g_1,b_{\text{green}})$ does not unify with $mark(g_1,b_1)$, where $b_1$ is the leftmost and marked box. This insufficiency is easily fixed using Reformation 3s, by replacing $b_1$ with $b_{\text{green}}$ in axiom $mark(g1,b1)$.

In $g_2$, $\mathbb{T}$ has both incompatibility and insufficiency faults, namely:

The simple repair that worked for $g_1$ will not work for $g_2$ because both $select(g_2,b_{\text{green1}})$ and $select(g_2,b_{\text{green2}})$ have to be proved and $b_1$ cannot be merged with both $b_{\text{green1}}$ and $b_{\text{green2}}$ because they are unequal.

Instead, ABC repairs the faulty $\mathbb{T}$ using the operation Belief Revision 2, namely adding extra preconditions to rule 5.1. This rule is duplicated and the two new rules are given different preconditions to distinguish the two situations: when there are more harmful than helpful boxes or the other way around. These two new rules are

and where $hm$ is the number of harmful boxes and $hp$ the number of helpful ones in the game. Using rule 5.3, the repaired theory suggests opening all boxes that are not marked.⁷ With these new rules, the repaired theory is able to correct the incompatibility and both the insufficiencies.

(c) Root cause analysis

Root cause analysis (RCA) diagnoses faults in a network system using system logs,⁸ where single causes can trigger multiple failures. Taking the input theory, containing the information from system logs and domain rules, ABC can detect missing information (MI) that is essential to cause failures and then suggests repairs that fix root causes [25].

Figure 7a shows the damage caused by MI in RCA. All nodes are explicitly in the theory, which models the software system, except the dashed node.⁹ Due to MI, the green node will not be diagnosed as the root cause of all four failures, as it should be. Figure 7b depicts ABC’s workflow in RCA, where the faulty $\mathbb{T}$, which lacks MI, is repaired into ${\mathbb{T}}_1$ to cover the previous missed information and then ${\mathbb{T}}_2$ includes repairs that fix root causes.

• Download figure
• Open in new tab
• Download PowerPoint

The example given by Li & Bundy [25] is about microservices in a network system. In the first step of RCA, ABC detects two insufficiencies in the original faulty theory, because the theory fails to predict two microservices failures. The first insufficiency is caused by the MI of a microservice session: that $id$ is built on a full board $d1$. Thus, the repair is to add the corresponding axiom (5.4) (in green). The other insufficiency is cased by the mismatch between the predicate $microservice$ in (5.5) and the predicate $ms$ in (5.6) (in red). The repair is to merge them, e.g. rename $ms$ to $microservice$. In the second step of RCA, ABC changes the full board to not being full, which solves all system failures: two microservices $id1$ and $id2$ deployed on that board and another microservice $id3$ depends on the failed $id2$ according to rule (5.6).

In this example, the two insufficiencies are caused by the incompleteness of the system log: the information of (5.4) was missing, and the theory is formalized from multiple data sources which caused the mismatch between (5.5) and (5.6), respectively. Then the repair of the former reminds engineers to improve the log quality by adding the MI. The repair of renaming $ms$ to $microservice$ contributes to aligning the knowledge from the different data sources. In addition, the repair of the second step of RCA provides the solution of fixing these system failures: ensuring that board $d1$ is not full.

(d) New physics by analogy

For his 2016 MSc project, Cheng-Hao Cai applied reformation to the problem of correcting faulty analogies [13,26]. One of these faulty analogies was between gravitational attraction and electrostatic attraction/repulsion. In particular, an approximation to Coulomb’s law of electrostatic force can be generated from Newton’s law of universal gravitation

where $F$ is the gravitational force acting between two objects of mass $m_1$ and $m_2$, $r$ is the distance between their centres of mass and $G$ is the gravitational constant. However, corresponding electrostatic charges repel rather than attract and $G$ must be replaced by Coloumb’s constant $k_e$.

2016 predates ABC, so Cai applied just reformation. He also needed equational reasoning in addition to resolution, so adapted reformation to work with the Z3 solver [27]. The equivalents of Reformation 1s was used to change attraction to repulsion and Reformation 3s to change $G$ to $k_e$.

(e) Modelling student misconceptions

When students learn arithmetic, they may make mistakes. Jovita Tang’s 2016 MSc project used reformation to model students’ misconceptions of arithmetic procedures [28]. The preferred structure was the students’ incorrect answers to arithmetic problems $\mathcal{T}(\mathbb{P}\mathbb{S})$, with the correct mathematical calculation rules $\mathbb{R}$ treated as the original faulty theory. ABC repaired $\mathbb{R}$ into a theory that models the student’s incorrect mathematical calculation, i.e. theory ${\mathbb{R}}^{\prime }$ is a logic program that derives the student’s miscalculations in $\mathcal{T}(\mathbb{P}\mathbb{S})$ as theorems. The repairs required to do this highlight the student’s misconceptions.