Humans are smart in revising their knowledge and concepts based on observations when they find conflicts. This ability to repair representations is also important for AI agents so that they can represent their environment correctly. This paper gives an overview of the domain-independent ABC system for repairing faulty logical theories by combining three existing techniques: abduction, belief revision and conceptual change. (A) Given an observation, represented as an assertion, and a current theory, abduction adds axioms, or deletes preconditions, which explain that observation by making the corresponding assertion derivable from the expanded theory. (B) Belief revision incorporates a new piece of information which conflicts with the input theory by either deleting old axioms or adding new preconditions to them. (C) Conceptual change uses the reformation algorithm for blocking unwanted proofs or unblocking wanted proofs. The former two techniques change an axiom as a whole, while reformation changes the language in which the theory is written. These three techniques are complementary so they are combined into one system: the ABC repair system, which is capable of repairing logical theories with better result than each individual technique alone and has been applied to applications in multiple domains. Datalog is used as ABC's underlying logic of theories, but the proposed system has the potential to be adapted to theories in other logics. Knowledge representation, Automated reasoning Automated agents use a representation of their environment (i) to interpret incoming sensory data, (ii) to infer new knowledge from old, (iii) to make plans to achieve their goals, and (iv) to predict the consequences of their actions and those of other agents. These environmental representations, which can be formalised as logical theories, are not static. They must change (i) when the environment changes, (ii) when the agent must deal with new kinds of goals, or (iii) when the agent detects that they are erroneous. Automated theory repair systems are proposed to address representation changes based on the proof of falsehoods [1, 2, 3]. Some repair systems are complementary in terms of the faults they tackled and the repair operations they generated. Thus, the ABC repair system is developed to combine abduction, belief revision and conceptual change for International Workshop on Human-Like Computing (HLC 2022), 28 -30 Sept. 2022, United Kingdom ∗The corresponding authors.
1. Introduction © 2022 Copyright for this paper by its authors.
Use permitted under Creative Commons License Attribution 4.0
International (CC BY 4.0).
generating more diverse repairs in a domain independent manner. No human interaction
is involved in ABC’s procedure but it may be necessary in particular applications, e.g.,
ABC is applied twice in a row in the root-cause analysis (RCA) [
There are abduction techniques based on machine learning approaches, e.g., [
In ABC, a Datalog-like theory [
Example 1. Virtual Bargaining Game Theory. • Modelling virtual bargaining game theory. In this game, human players need to guess or adjust the winning strategy based only on others’ game moves. Given this limited bandwidth, each player has to imagine what the other is thinking and plan their play too, so called virtual bargaining. To model this process, the game setups and a candidate of original winning strategies are given as ABC’s input theory and 1We only give the example of the virtual bargaining in this paper. Other examples can be found in the cited papers.
the desired game movement as the benchmark of () and ℱ () , as in Example 1.
ABC will repair the candidate into correct winning strategies, given by Example 2.
It is particularly useful when the game setup is changed so the previous winning
strategy (A1 in Example 1) is outdated [
Example 2. Repaired Virtual Bargaining Game Theory.
< ( , ℎ, ℎ) ∧ ( , ) ⟹
( , )
< ( , ℎ, ℎ)∧ ≠ ( , ) ∧ ( , )
2. The ABC Repair System
ABC repairs incompatibility and insuficiency by combining diferent repair approaches.
Thus, ABC has richer repair operations that are not only adding or deleting axioms; it
can also rewrite the language of the theory, e.g., rename a constant/predicate or adapt
the arity of a predicate. Particularly, ABC can add/delete preconditions from existing
rules or create new rules. More details about ABC’s repair operations w.r.t. a (possibly
failed) proof can be found in [
C4. Prune the Sub-optimal Inputs: , ℙ
C1. Pre-Process
C2. Detect Faults
Faultfree
No
Yes Success C3. Repair Faults Fail (MSCR)
Output: {′1, !2 … }
Drop
The pipeline of ABC is given by Figure 1. Datalog is a declarative logic programming
language in first-order logic. Currently, ABC is restricted to repair Datalog-like theories,
i.e., a piece of Datalog program is seen as a logical theory based on Datalog logic. Datalog
is chosen because its deduction is decidable [
C1 is a pre-process which checks whether the is self-contradictory and calculates minimal sets of axioms by pruning redundancy. It reduces the search space of both fault detection and repair generation. Given a minimal axiom set, faults are detected by C2. If there is no fault, then the theory is collected as an output. Otherwise, the information about the fault, which could be either proofs or failed proofs, is provided to C3 to generate repairs. If no repairs can be found or the resource threshold2 is reached, the process will be terminated with a failure to find any repaired theories.
Otherwise, C3 generates all possible repairs for all detected faults in parallel. When
repairs which individually aim at diferent faults change diferent parts of the theory, they
can be applied at the same time, called commuting repairs. C3 computes maximal sets
of commuting repairs (MSCRs) and then applies each MSCR respectively to reduce the
search space3. Then C2 will check the remaining faults of these semi-repaired theories one
by one. Based on the number of the remaining faults and the applied repair operations,
sub-optimal theories will be pruned by C4 [
Acknowledgments This research has been supported by the Huawei funded TREAT project CIENG4721/LSC. The first author gratefully acknowledge the support of ELIAI (The Edinburgh Laboratory for Integrated Artificial Intelligence) EPSRC (grant no EP/W002876/1) and the second author of UKRI grant EP/V026607/1. Meanwhile, great thanks to the HCL 2022 reviewers for their useful feedback, which improved the paper. For the purpose of open access, authors have applied a Creative Commons Attribution (CC BY) licence to any Author Accepted Manuscript version arising from this submission.
Appendix: Examples of Conceptual Change Two examples of conceptual change are given in this appendix, together with one of their best repaired theories generated by the ABC system. Changes in repaired theories are highlighted in red.
• The Theory is repaired by enriching the constant ℎ 1 , which illustrates a conceptual change. into a variable in Example 3. Families Theory.
( , , ℎ) ⟹ ( , ) () = { (, ), (, )} ℱ () = ∅ ⟹ (, , ℎ) ⟹ (, , )] (A1) (A2) (A3) x a m p l e , ) ⟹ ⟹ ⟹ ( , ) ( , ( , , , ℎ
) )
] () = { ( , ) , ( , ) } ℱ () =
∅ E x a m p l e 5 .
T w e e t y
T h e o r y . ( ) ⟹ ( ( ) ) (
) ⟹ ⟹ ℎ (
) (
) ⟹ ⟹ (
) , ) } ℎ ( ) , ( ) } E x a m p l e 6 .
R e p a i r e d
T w e e t y
T h e o r y w h i l e p e n g u i n o
f 1 ) ( A 1
) ( A 2
) ( A 3
) ( A 1
) ( A 2
) ( A 3
) ( A 4
) ( A 5
) ( A 1
) ( A 2
) ( A 3
) ( A 4
) ( A 5 ) ( ) ⟹ ( , 2
) ( , ( , 1 ) ) ⟹ ⟹ ⟹ ⟹ ℎ (
) (
) ( , , ) } ℎ ( )