## Abstract

Automated reasoning is an enabling technology for many applications of informatics. These applications include verifying that a computer program meets its specification; enabling a robot to form a plan to achieve a task and answering questions by combining information from diverse sources, e.g. on the Internet, etc. How is automated reasoning possible? Firstly, knowledge of a domain must be stored in a computer, usually in the form of logical formulae. This knowledge might, for instance, have been entered manually, retrieved from the Internet or perceived in the environment via sensors, such as cameras. Secondly, rules of inference are applied to old knowledge to derive new knowledge. Automated reasoning techniques have been adapted from logic, a branch of mathematics that was originally designed to formalize the reasoning of humans, especially mathematicians. My special interest is in the way that representation and reasoning interact. Successful reasoning is dependent on appropriate representation of both knowledge and successful methods of reasoning. Failures of reasoning can suggest changes of representation. This process of representational change can also be automated. We will illustrate the automation of representational change by drawing on recent work in my research group.

## 1. The automation of reasoning

Reasoning can be automated by drawing on the formalisms provided by mathematical logic.

—

*Knowledge is represented as a set of axioms in a logical theory.*For instance, the knowledge that*Elizabeth*is female might be represented by the axiom:*Female*(*Elizabeth*), where*Female*is a*predicate*that given a person returns a truth value: true or false. The knowledge that Elizabeth is the mother of Charles might be represented by the axiom:*Mother*(*Charles*)=*Elizabeth*, where*Mother*is a function that given a person returns their mother. Functions and predicates take a fixed number of*arguments*(aka inputs or parameters). In our examples,*Female*takes one argument, namely*Elizabeth*, and*Mother*also takes one argument, namely*Charles*. They are, therefore, called*unary*. An example of a binary predicate, i.e. one taking two arguments, would be*Loves*(*Elizabeth,Charles*).— These examples are written in the language of first-order logic. A formal definition of this language is given in §1

*b*.—

*General purpose rules of inference are used to infer new theorems from axioms and previously proved theorems.*For instance, the*modus ponens*rule of inference is The two premises of this rule, which are written above the horizontal line, are that*P*is true and that if*P*is true then*Q*is true. The conclusion of the rule, which is written below the line, is that we can deduce that*Q*is true. The history of modus ponens goes back to antiquity. We will refer to the sets of axioms and rules as*logical theories*, but they are also sometimes called*ontologies*or*knowledge bases*.*Representation*is the process of formalizing real-world knowledge in a logical theory.—

*An automated theorem prover is used to apply rules of inference to axioms and old theorems to derive new theorems.*For instance, if our axioms include*Mother*(*Charles*)=*Elizabeth*and*Mother*(*c*)=*m*⇒*Female*(*m*) then a prover could use modus ponens to derive*Female*(*Elizabeth*). Note that*c*and*m*are variables that range over people and that one of the operations involved in applying a rule of inference is to match variables, such as*m*, to constants, such as*Elizabeth*, and to instantiate such variables to the matching constant—or, more generally, to compound terms, such as*Mother*(*Charles*). We will refer to the process of proving theorems as*reasoning*. Note that automated reasoning is often performed backwards: from a conjecture to be proved towards the axioms, i.e. the conclusion is matched to a conjecture and then an attempt is made to prove the premises as new conjectures or*sub-goals*. The process terminates with success when all the outstanding sub-goals can be matched to axioms.

### (a) Applications of automated reasoning

Automated reasoning is a key enabling technology in Informatics. It is applied, for instance, in the following areas:

*Reasoning about programs*. To ensure that programs have been written correctly, it is possible to prove that they meet a specification of their behaviour. For instance, a program to sort a list of elements into alphabetic order can be formalized as a logical function and shown to output a list that is an ordered permutation of its input. This area is called*formal methods*. It can be used to show that a program is safe, secure and reliable for an infinite number of possible inputs, whereas program testing is inherently restricted to a finite set of inputs.*Forming plans*. Artificial agents, such as autonomous robots, must form plans to achieve the goals they are set. The initial state of the agent's environment and the actions it can perform can all be represented as axioms and the goal as a conjecture to be proved. A proof that the goal can be achieved by executing a sequence of actions can then be interpreted as the required plan.*Question answering*. Questions can be answered by combining information stored, for instance, on the Web or in databases. The known information can be represented as axioms and the question to be answered as a conjecture to be proved. The proof of this conjecture is a theorem that can be interpreted as showing how the answer to the question follows from already known information.

### (b) The language of first-order logic

Axioms, theorems and other formulae of first-order logic are expressed in a formal language, which we describe in the following definitions.

Terms are used to describe objects of the domain. The domain is the collection of entities that a logical theory formalizes.

### Definition 1.1 (Terms)

A *term* is either constant, a variable or an *n*-ary^{1} function applied to *n* terms. In our examples, *Charles* is a constant, *c* is a variable, *Mother* is a unary function and *Mother*(*c*) is a compound term.

We will adopt the notational convention that variable names start with a lower case letter, and constant, function and predicate names start with an upper case letter.

Propositions are used to describe individual facts and goals about these domain objects.

### Definition 1.2 (Propositions)

A *proposition* is a truth value ⊤ (meaning true) or ⊥ (meaning false) or an *n*-ary predicate applied to *n* terms. In our example, *Loves* is a binary predicate and *Loves*(*Elizabeth*,*c*) is a proposition.

Formulae are constructed from propositions using logical connectives and quantifiers.

### Definition 1.3 (Formulae)

A *formula* is a proposition, an *n*-ary connective applied to *n* formulae or a quantifier applied to a variable and a formula (usually containing that variable). We will use the following connectives:

*Negation*. ¬*P*is true if and only if*P*is false;*Conjunction*.*P*∧*Q*is true if and only if both*P*and*Q*are true;*Disjunction*.*P*∨*Q*is true if and only if either*P*or*Q*is true (or both);*Implication*.*P*⇒*Q*is true if and only if whenever*P*is true, then*Q*is true;

and the following quantifiers:

*Universal*. ∀*x*.*P*(*x*) is true if and only if*P*(*c*) is true for all*c*in the domain quantified over;*Existential*. ∃*x*.*P*(*x*) is true if and only if*P*(*c*) is true for at least one*c*in the domain quantified over.

We will use the term *expression* when we do not want to distinguish between terms, formulae, functions, etc.

When the domain is not uniform, but consists of different kinds of objects, it is often useful to distinguish the different kinds of objects to which expressions refer. Then quantification, for instance, can be restricted to range only over objects of one kind. This can be done by assigning sorts or types to expressions. We will encounter such a typed logic in §5. Example types are , the type of real numbers, , the type of truth values, and , the type of people. We will use *e*:*τ* to assert that expression *e* has type *τ*, and we will use *τ*, possibly subscripted, to range over types. We can also assign types to functions, predicates, connectives, quantifiers, etc. For instance, means that *Mother* is a function from people to people, where ↦ represents that one type of object is converted into another. Such type structures can get quite complicated. For instance, the quantifier ∀ can be considered to take a unary predicate and convert it to a truth value, which we can represent with the assignment . Note the use of the type variable *τ*, which indicates that the argument of the unary predicate can be of any type. When something has type variables in its type, it is called *polymorphic*.

A logical theory can be represented as a pair , where is the *signature* of the ontology and is a set of axioms. is a set of declarations of the types of the various constants, functions and predicates which are used in formulae of . It can be used as the basis of a recursive definition of the language of the theory, i.e. we can define the terms, formulae, etc., in terms of the constants, functions and predicates declared in the signature. For instance, we might define a theory *Family* with:
and
We will write to mean that is a theorem of . For instance, *Family*⊢*Female*(*Elizabeth*).

### (c) The resolution rule of inference

A common rule of inference used in the automation of inference in first-order logic is *resolution* [1]. This rule is described in definition 1.6. Resolution uses *clausal form*, *substitution* and *unification*, which are described in §1*c*(i),(ii).

#### (i) Clausal form

Binary resolution applies to two clauses and derives a third clause. The axioms of a first-order theory are transformed into an equivalent conjunction of clauses. The conjecture to be proved is negated and also transformed into a conjunction of clauses. These two conjunctions are themselves conjoined and resolution is repeatedly applied to them.

### Definition 1.4 (Literals and clauses)

A *literal* is either a proposition or a negated proposition. A *clause* is a disjunction of literals. The empty clause is represented by , which is logically equivalent to ⊥ (false).

Resolution proofs work by *reductio ad absurdum*,^{2} i.e. the conjecture is negated and the aim is to infer the empty clause (false). The original conjecture is then proved.

To transform a formula into *clausal form*, it must be reorganized so that:

— ¬ only appears in front of propositions, not compound formulae.

— ∨ only disjoins literals.

— ∧ only conjoins clauses.

— ∀ and ∃ are eliminated in a process called

*skolemization*. Universally quantified variables are regarded as implicitly universal and the quantifier is removed. The previous universally quantified variable is now called a*free variable*. Existential quantified variables are transformed into new*skolem functions*, whose arguments are just those universal variables that are quantified before the existential one.

For instance, the definition of a continuous function is
1.1Skolemizing this formula gives
1.2where *Δ* is a new, binary skolem function. Note that *Δ* has *x* and *ϵ* as arguments, but not *b*, because, reading left to right, *x* and *ϵ* are quantified before *δ*, but *b* is quantified afterwards.

This skolemized formula can now be transformed into two clauses: 1.3

Suppose that instead of using formula (1.1) as an *axiom* to assert the continuity of a function, we wanted to prove the continuity of a function as a *theorem*. Formula (1.1) would now have to be negated before putting it into clausal form.
We use the equivalences
to move the ¬ inside the quantifiers to give
Skolemizing this formula then gives
1.4Compare formula (1.4) with (1.2). Note how the free variables and skolem functions swap roles as a result of negation.

This skolemized formula can now be transformed into the following three clauses: 1.5Compare the clauses (1.3) with (1.5). Note how the roles of ∨ and ∧ are swapped and how negated literals become unnegated and vice versa.

#### (ii) Substitutions and unification

A substitution is used to create an instance of a term or formula. It consists of a set of instructions to replace variables with terms.

### Definition 1.5 (Substitution)

A *substitution* is a set of pairs *x*_{i}/*s*_{i}, for 1≤*i*≤*n*, where the *x*_{i} are distinct variables and the *s*_{i} are terms that contain none of the *x*_{j} for 1≤*j*≤*n*.

We will use *σ*, possibly subscripted, to represent substitutions.

We write *tσ* to mean the term *t* with the substitution *σ* applied to it. For instance, *Loves*(*x*,*y*){*x*/*Elizabeth*,*y*/*Charles*} evaluates to *Loves*(*Elizabeth*,*Charles*).

Unification is an algorithm for creating substitutions. Given two terms or propositions, say *s* and *t*, it will, if it is possible, create a substitution *σ*, called a *unifier*, such that *sσ* and *tσ* are identical. It also creates the most general such unifier, i.e. it does not instantiate any variable strictly more than necessary to make the two terms/propositions identical. For instance, the most general unifier of *Loves*(*Elizabeth*,*y*) and *Loves*(*u*,*v*) is {*u*/*Elizabeth*,*v*/*y*}. The substitution {*u*/*Elizabeth*,*v*/*Charles*,*y*/*Charles*} would also be a unifier, but not the most general one in this case. If variations in the names of variables are ignored, most general unifiers are unique. A version of the unification algorithm adapted from [2], p. 455 is described in table 1.

We are now in a position to define the *binary resolution rule*.

### Definition 1.6 (Binary resolution)

where the *P*_{i} are propositions, the *C*_{i} are clauses and *σ* is the most general unifier of *P*_{1} and *P*_{2}.

The unification algorithm finds a substitution, *σ*, that makes *P*_{1}*σ* identical to *P*_{2}*σ*. A new clause is then formed by disjoining the remaining literals *C*_{1} and *C*_{2}, then applying *σ* to all the literals in the new clause. Modus ponens is a special case of resolution. An example of binary resolution is:
where *P*_{1} is *Mother*(*Charles*)=*Elizabeth*, *P*_{2} is *Mother*(*c*)=*m* and *σ* is {*c*/*Charles*,*m*/*Elizabeth*}.

Binary resolution needs to be supplemented with the *factorization rule.*^{3} Factorization merges several literals in a clause into one by applying their most general unifier to the clause, so that these literals become identical. The combination of binary resolution and factorization is *complete*, meaning that if a conjecture is provable from some axioms, then these two rules will find a refutation, i.e. will prove . If, however, the conjecture is not provable, then

— either a stage will be reached at which no further rules are applicable, but has not been proved, or

— the rules may keep on finding new clauses without terminating.

Because of this potential for non-termination, resolution is *semi-decidable*, i.e. it may never decide the question of whether a conjecture is a theorem, since the fact that it has not terminated yet does not mean that it would not eventually.

## 2. Reasoning failures and possible repairs

We are interested in how reasoning failures can trigger representational change. Moreover, we focus on *conceptual* change, i.e. not just the deletion or addition of axioms in a representation, but a change in the *language* in which the axioms are expressed. Typical language changes include the splitting of a function (or predicate) into two or more functions (or predicates); the merging of two distinct functions (or predicates) into one; and a change in the number of arguments that a function (or predicate) takes, e.g. by removing or adding one or more of them.

We will consider the following kinds of reasoning failure:

*Proof of a false conjecture*. If a false conjecture can be proved in a logical theory, then it can be repaired either by removing one or more axioms or rules, or by changing the language in which one or more of them are expressed. For instance, suppose it is possible to prove both*Capital*(*Japan*)=*Tokyo*and*Capital*(*Japan*)=*Kyoto*,^{4}where*Capital*is a function that takes a country and returns its capital city. If either of these theorems is an axiom, then the representation can be repaired by removing one of them. Alternatively, since Kyoto used to be the capital of Japan, we could retain this information by introducing a new function*WasCapital*and a replacement axiom*WasCapital*(*Japan*)=*Kyoto*. Or we could add an additional time argument to*Capital*, e.g. with replacement axioms*Capital*(*Japan*,*Now*)=*Tokyo*and*Capital*(*Japan*,*Past*)=*Kyoto*.^{5}*Failure to prove a true conjecture*. If we cannot prove something that is true then we can repair the representation by adding a new axiom or rule, or by changing the language. For instance, suppose that*Female*(*Elizabeth*) is not a theorem. Perhaps, the axiom*Mother*(*Charles*)=*Elizabeth*is missing, so we could add it. Alternatively, perhaps the axioms we were hoping to derive*Female*(*Elizabeth*) from are*Mother*(*Charles*)=*Elizabeth*and*MumOf*(*c*)=*m*⇒*Female*(*m*), where*Mother*and*MumOf*are two different names for what was intended to be the same function. This might happen, for instance, if the representation has been formed by merging two different ones, or if multiple authors of a representation have been working at cross purposes as to the correct name for this function. The representation could then be repaired by renaming, say,*MumOf*to*Mother*, or vice versa. Figure 1 describes how an everyday object can be formalized in two different ways, and making the correct choice between them is crucial for success.*Reasoning runs out of resources*. Reasoning is computationally expensive. Multiple rules are often applicable to each (sub-)goal, perhaps in multiple ways, and each may need to be tried during a proof attempt. The number of alternative proof attempts can grow exponentially (or worse) in the length of the proof to be discovered. So reasoning can fail due to exhaustion of resources, e.g. the time or the storage available. As Pólya has emphasized, however, successful problem solving is very dependent on finding an appropriate representation [4]. In a better representation, a more succinct proof may be possible or one requiring less search. Figure 2 describes the Mutilated Checker Board^{6}Problem, in which a change of representation makes a dramatic difference to the efficiency of problem-solving and the understandability of the solution.

Representational changes of the kind illustrated earlier are frequently manually applied to computer representations as part of development and maintenance. Automatic addition and removal of axioms has also been implemented in the fields of abductive reasoning and belief revision, respectively. These two fields are briefly discussed in §8. Automated conceptual/language change is less common, but has been pioneered in my research group, examples of which will be given below.

## 3. Why is automated representational change important?

Automated agents are becoming more of a feature of high-tech applications. They range from industrial, domestic and military robots, to purely software agents in personal mobile devices, to programs used in finance and commerce, e.g. to buy and sell financial instruments. Such agents require representations of their environment, including representations of the representations of other agents, to form plans, negotiate transactions, answer questions, etc. Until recently, such agents worked in a relatively stable environment and on a relatively stable task, which meant that their representations could also be stable. Typically, these representations were built manually by the designer of the agent and any changes required would also be handled manually during upgrades.

No universal representation is possible. The world is infinitely rich and any representation is an approximation of that richness. The designer of a logical theory must find a sweet spot between expressivity and efficiency; that is, the theory must be rich enough for the agent to perform its task, but simple enough for automated reasoning to be tractable. The agent's representation will be tuned to its role.

Many future applications of automated agents will, however, require them to adapt to a changing environment and a changing role. Representational change will be required:

— to accurately model changes in the environment;

— to ensure that reasoning is appropriate for any new reasoning task the agent is set; and

— to enable communication with other agents which are using different representations of the environment.

Sometimes the need for representational change will be sufficiently urgent that it cannot wait on the designer to make manual changes, but must be automatic and dynamic, i.e. implemented while the agent is still reasoning [6]. Consider, for instance, emergency response. In an emergency, multiple agencies must collaborate to solve problems, some of which are unforeseen. In a flood, police, health services, fire brigade, the military, local government, the meteorological office, various NGOs, etc., must collaborate in a rapidly changing situation. This collaboration will include the sharing of information stored digitally in different formats. Automated and dynamic alignment and updating of these different information sources is essential. Failures due to lack of effective communication are frequently cited in post-emergency reports, so this is a real problem, which is likely to increase in importance as the rate of emergencies increases as a side-effect of climate change.

## 4. Repairing an agent's representation of other agents

The ORS (Ontology^{7} Repair System) [6] uses a planning agent's representations of the services provided by service-providing agents to construct a plan composed of those services. For instance, the planning agent might plan a holiday by composing the services provided by airlines, hotels, tour providers, etc. Its representations of these other agents may, however, be inaccurate. If so, then its plan may fail to execute, for instance, a service-providing agent may refuse to provide its expected service. ORS then tries to diagnose the cause of the failure, repair the planning agent's representations to be a better match to those of the service-providing agents, then re-plan: repeating this process until either a plan succeeds or it is unable to diagnose the cause of failure and/or repair the faulty ontology.

The services provided by the service-providing agents are represented by STRIPS-like planning operators [7]. These describe the preconditions under which an agent will provide a service and the effects of doing so. ORS's diagnosis process works by considering the *execution* of the plan as a *failed* proof of a true conjecture: that is, it assumes that there is a plan that will achieve its goals, but that it has failed to find it. It uses clues from the failed execution of the unsuccessful plan to diagnose the errors in its representation.

One such clue is a *surprising question*. The planning agent expects to be asked certain questions during the course of the execution of its plan. These questions might arise, for instance, when a service-providing agent is checking the preconditions of its service. Some of these preconditions it can check itself, but some have to be directed to the planning agent, which expects these questions. Communication between the agents takes the form of logical formulae, sometimes containing variables that the recipient is asked to instantiate and return the values of. For instance, a hotel agent might ask whether the planning agent has the deposit for a room. The planning agent might expect this question to take the form *Money*(£ 200). Suppose that this question is not asked, but that the surprising question *Money*(£ 200, *Credit_Card*) is asked instead. ORS can make a fuzzy match between the expected and the surprising question and infer that the planning agent has a unary version of *Money* but that the hotel agent has a binary one. Moreover, the second argument is *Credit*_*Card*, i.e. the hotel requires to be paid the deposit by credit card, whereas the planning agent thought any form of payment was acceptable.

ORS must now update the planning agent's ontology by changing its unary predicate *Money* to a binary one. In the precondition of the hotel's service, the second argument of this predicate must be *Credit*_*Card*. The planning agent will now replan with this new representation and try to execute the new plan. Sometimes multiple cycles of this plan, diagnose and repair process are required before a successful plan is formed.

## 5. Repairing physics theories

The GALILEO System (Guided Analysis of Logical Inconsistencies Leads to Evolved Ontologies) suggests repairs to faulty theories of Physics when they are contradicted by reliable experimental evidence [8]. GALILEO has one ontology to represent the theory and another to represent the conflicting experimental evidence.

GALILEO uses a number of what we call *ontology ^{8} repair plans* (ORPs). Each ORP consists of a trigger formula and some representation repair instructions: when the trigger formula can be proved, the repair is executed. The trigger formula describes theorems of two or more ontologies, which taken together are in conflict, e.g. are inconsistent. The most commonly applicable ORP is Where's My Stuff (WMS figure 3). Its trigger formula is:
where the are distinct ontologies: might be the representation of a Physics theory; that of some conflicting experimental evidence and the representation of a theory of arithmetic. Some attribute

*f*of some stuff is predicted to take the value

*v*

_{x}, but experiment shows it to have a different value

*v*

_{y}.

First-order logic is not ideal for representing many aspects of Physics as it is often desirable to have variables ranging over functions and to have functions that take other functions as arguments. Consider, for instance, differential calculus, where the differentiation operation is naturally represented as a function that converts one unary function into another. For this reason, logical theories in GALILEO are represented in higher-order logic, which permits function variables and functions of functions.

Associated with the WMS trigger is a particular form of repair. New versions of and are constructed, which we will call and , respectively. Recall from §1*a* that an ontology can be represented as a pair of sets of the type declarations (the signature) and the axioms: . For instance, the set of type declarations {stuff *τ*, *v*_{x}*τ*′,*f*:*τ*↦*τ*′} means that stuff is of type *τ*, *v*_{1} is of type *τ*′ and *f* is a function from things of type *τ* to things of type *τ*′. Typical types in GALILEO are be real numbers, graphs, galaxies of stars, etc.

The signatures for the new ontologies are updated in terms of those of the old as follows:
and
That is, two new objects, stuff_{vis} and stuff_{invis} are created with the same type as stuff. The idea is that stuff will now be divided into visible and invisible stuff. They are both added to the signature of , and stuff_{vis} is used to replace stuff in . So in we can refer to visible, invisible and total stuff, but in we only refer to visible stuff.

The axioms for the new ontologies are updated in terms of those of the old as follows:
and
contains all the axioms of but also has a new axiom that connects the three kinds of stuff: invisible stuff is defined as the difference between total stuff and visible stuff. −_{τ} is a form of subtraction that is appropriate for objects of type *τ*. For instance, if *τ* is the real numbers then −_{τ} will be ordinary subtraction, but if *τ* is a set then −_{τ} will be set minus. contains all the axioms of , but with every occurrence of stuff replaced with stuff_{vis}.

The new version of the trigger formula no longer suggests a conflict. is now an observation only about visible stuff, so does not contradict , which is about total stuff.

## 6. Repairing faulty mathematics proofs

In [9] (appendix I), Lakatos describes Cauchy's faulty proof that the limit of a convergent series of continuous functions is itself continuous. Fourier analysis had provided a counter-example to this faulty theorem. One can give a convergent series of (continuous) sine functions whose limit is the (discontinuous) square wave. For a long while, even though this counter-example was known, the error in the proof lay undiscovered. Its eventual repair was to replace ‘convergence’ with ‘*uniform* convergence’ in the theorem's premise. The only difference between these two concepts is the quantifier order.

*Convergence*.*Uniform Convergence*.

Note that ∀*x* is moved from being the first quantifier in convergence to being the third in uniform convergence.

In the study of Bundy [10], we noted that the error in Cauchy's proof can, when represented as a resolution proof attempt,^{9} be described as an *occurs check* error. That is, there is an unsuccessful attempt to resolve
where *M*, *E*, *B* and *Δ* are skolem functions arising from the existentially quantified variables *m*, *ϵ*, *b* and *δ* in the definitions of convergence and continuity. This resolution step will fail due to an application of step *Occurs* in the unification algorithm described in table 1, since the *Occurs* condition is true. The context in which this failed resolution step arises is described in figure 4.

One way to repair this faulty proof is to enable the blocked resolution step to succeed. For this, it is necessary to remove the embedded *n* from *M*(*x*+*B*(*Δ*(*E*/3,*x*,*n*)),*E*/3). Since this unwanted *n* is embedded in three skolem functions: *M*, *B* and *Δ* this can be done by reordering the quantifiers in the definitions of convergence or continuity. For instance, *m* has two arguments because it is preceded by two universally quantified variables: *x* and *ϵ*. We want to remove its first argument, which is supplied by the ∀*x*. This can be done by moving ∀*x* after ∃*m* in the definition of convergence. This gives the desired definition of uniform convergence. Now the previously faulty resolution step is replaced by
which succeeds since .

The variable *n* was, though, originally nested within two other skolem functions: *B* and *Δ*, so two other repairs are also suggested.

—

*B*is a skolem function that arises from the definition of continuity when it is negated, since the originally universally quantified*b*becomes existentially quantified when the ¬ is moved inwards (formula (1.4)). To effect this repair, we need to move ∃*δ*>0 after ∀*b*, i.e. This, however, is a trivial property that holds for all functions, so does not suggest a sensible corrected theorem.—

*Δ*is a skolem function that arises from the definition of continuity in the following form: where*S*(*n*,*x*) is the finite sum of the*f*_{i}up to*n*, i.e. . To effect this repair, we need to move the after the ∃*δ*>0 to obtain This concept was independently discovered by Ascoli, who called it*equi-continuity*[11]. It leads to a different and interesting repair of Cauchy's theorem in which the*f*_{i}are equi-continuous. Ascoli also proved a theorem about equi-continuity, but not this one.

## 7. Reformation: a domain-independent algorithm for representation language repair

In §§4–6, we have described domain-specific algorithms for repairing the languages in which representations are formalized. Is there a general-purpose algorithm that subsumes them all? We are developing such an algorithm, which we call *reformation* [12].

Reformation is designed to deal with two of the three types of failure described in §2: the proof of a false conjecture and the failure to prove a true conjecture. It is adapted from the unification algorithm, described in table 1. The unification rules have been reordered into complementary pairs. The members of each pair share the same Before pattern, but have opposite Conditions: with one member a success case and the other a failure case. The algorithm deals both with situations in which a successful unification must be blocked and those in which an unsuccessful one must be unblocked. Blocking works by switching a success case to a failure one; unblocking works by switching a failure case to a success one. The algorithm is described as a set of transformation rules in table 2.

Note that reformation is completely automatic, i.e. no human intervention is required for it to suggest repairs. Both blocking and unblocking are guaranteed to succeed, i.e. they always suggest one or more repairs that will either block unification, so that it fails, or unblock unification, so that it succeeds. Its efficiency is essentially the same as for unification, i.e. it is exponential in the size of the input problem. It is well known that the occurs check is the source of the exponential run-time, but linear versions of unification have been devised, so there is potential to adapt these more efficient versions of unification to construct a more efficient version of reformation. Unification is used in resolution provers that generate millions of intermediate clauses in tractable runtimes, so its efficiency does not seem to be a practical problem.

What is a practical problem, however, is the huge number of repairs that reformation suggests. For instance, a large resolution proof can be blocked in several ways at every step of unification in every application of resolution. Heuristics are needed to decide which blocking repair suggestion to adopt. For unblocking, the situation can be much better. If we have a candidate faulty proof, then this will typically only be blocked at a few resolution steps, so only these steps need to be repaired, leading to only a handful of unblocking repair suggestions. This is the case, for instance, for the example described in §6.

Reformation can be successfully applied to the examples in §§4–6.

*ORS*. In §4, we described a failed unification between*Money*(£ 200) and*Money*(£ 200,*Credit_Card*). When reformation is asked to unblock this unification, transformation rule*CC*_{f}is fired. It suggests making the arities of the two occurrences of*Money*be the same. One way to realize this repair is to add an additional argument to the first occurrence to make it identical to the second one.*Galileo*. In §5, the inconsistency can be formalized as arising from a successful but unwanted unification between two occurrences of*f*(stuff). When reformation is asked to block this unification, transformation rule*CC*_{s}is fired both on*f*(stuff)≡*f*(stuff) and then, recursively, on stuff≡stuff. It makes various suggestions, one of which is to distinguish the two occurrences of stuff by renaming one of them.*Faulty proofs*. In §6, we described a failed unification between*y*≥*y*and*n*≥*M*(*x*+*B*(*Δ*(*E*/3,*x*,*n*)),*E*/3). When reformation is asked to unblock this unification, transformation rule*V**C*_{f}is fired. It suggests removing*n*from*M*(*x*+*B*(*Δ*(*E*/3,*x*,*n*)),*E*/3). As we have seen, this can be done in three^{10}different ways, two of which lead to significant and interesting theorems.

More generally, our experience with reformation so far is that it has always found the theory repair that we had hoped to find, e.g. the repair proposed as desirable by some third party expert. It also, however, finds a huge number of additional repairs. Some of these additional repairs make intuitive sense and can be useful in expanding your thinking to some of the other viable possibilities. Many of the suggestions, unfortunately, do not make much sense. We are experimenting with heuristics to prune such unwanted suggested repairs. For instance, we protect some functions and predicates from repair, e.g. we do not allow either renaming or arity changing to, say, = or +.

## 8. Related work

Several different fields of AI have investigated the problem of changing logical theories.

*Belief revision*. Deals with the problem of adding a new belief to a theory that might result in it becoming inconsistent [13]. In this case, mechanisms have been designed to re-establish its consistency. These involve the identification of facts or (more rarely) rules to be deleted. Our work is complementary to this in suggesting changes to the*language*of the theory rather than the deletion of formulae.*Abduction*. Deals with the problem of identifying explanatory hypotheses for observations [14]. New facts or rules are identified as hypotheses which, when added as new axioms to the ontology, enable the observations to be deduced. Again, our work is complementary to this in suggesting changes to the*language*of the theory rather than the addition of new formulae.*Ontology evolution*. Deals with the problem of managing an ontology.^{11}Most of the work in this area consists of tools to assist manual construction and maintenance of ontologies. Our work differs in providing a tool for*automatic*identification of changes to the*language*of the ontology.*The ibis system*[15] presents an approach for automatic ontology repair in the context of description logic. The approach focuses on repairing inconsistencies in terminological hierarchies. This approach detects three types of inconsistencies in these hierarchies: polysemy, single over-generalization and multiple over-generalization. Polysemy occurs when a concept is subsumed by two disjoint concepts. Single over-generalization occurs when a concept is too specifically defined, so that one of its instances violates its definition. Multiple over-generalization occurs when two or more definitions of the same concept conflict with each other.The extended version of reformation for sorted logics [16] suggests all the repairs made by the ibis system, but also suggests additional sensible repairs. Reformation has, thereby, been shown to apply to description logic problems converted to first-order logic. This suggests that it will be possible to adapt reformation so that it applies directly to description logics.

*Abstraction*. Has been frequently used in automated reasoning. For instance, Giunchiglia & Walsh [17] survey the uses of abstraction to simplify the original problem, solve the simplified problem, then map the solution of the simplified problem to a solution to the original problem. In proposing theory repairs, our work uses both abstraction, e.g. merging functions, dropping arguments and refinement, e.g. splitting functions, adding arguments. ORS explicitly based its repairs on the abstraction classification proposed in the study of Giunchiglia & Walsh [17], augmented with refinement techniques that inverted these abstraction techniques. Later work, e.g. reformation, has built on this classification and, thereby, provided a generative theory that underpins it.*Different logics*. Are used to formalize representations in different areas of research. Some common alternatives to first-order logic are:*Higher order logics*. Which allow variables over functions, predicates, functions of functions, etc., as well as variables over domain objects. These variables can then be quantified. For instance, ∀*x*,*y*.*x*=*y*⇒∀*p*.*p*(*x*)⇒*p*(*y*) applies quantification to a unary predicate variable*p*. The work described in §5 represented both the theories and experiments of Physics and the ontology repair plans in higher order logic.*Sorted and typed logics*. Which assign a type to each constant, variable and (sometimes) functions and predicates too. This is useful when the domain contains a mixture of different types of object, e.g. people, places, vehicles, etc. The work described in §5 used a typed, higher order logic. Boris Mitrovic is currently extending reformation to various sorted first-order logics [16].*Description logics*. Are restrictions of first-order logic so that reasoning always terminates. For instance, they usually only allow unary and binary predicates and no functions. The OWL family of description logics (OWL Lite, OWL DL, OWL2 and OWL Full) have been recommended by the World Wide Web Consortium as standards for representing knowledge represented on the Internet [18].

Although we have mainly described our work in terms of first-order logic, the discussion above shows that many of the techniques apply to these other logics too.

## 9. Conclusion

In this paper, we have outlined how knowledge can be represented in logical theories and reasoning can be automated. We have emphasized the interaction of representation and reasoning: finding the right representation is the key to successful reasoning; failures of reasoning can suggest how faulty representations can be repaired. We have focused on two of the most common kinds of representational fault: a false conjecture can be proved; a true conjecture cannot be proved. We have illustrated the diagnosis and repair of faulty representations in three domains: multi-agent planning, physical theories and experiments, and mathematical proofs. This work illustrated that it is possible not just to assert or retract beliefs represented as axioms, but that conceptual change is possible via language repair. Finally, we have discussed the reformation algorithm: a general-purpose algorithm for the diagnosis and repair of faulty representation languages.

Over the next half century, the automated repair of formal representations is set to be a key research area in automated reasoning and machine learning [19]. Until recently, most formal representations have been manually designed, by skilled knowledge engineers, for a narrowly defined reasoning application. If repairs were necessary, they have also been performed offline and manually. This situation is now changing:

— automated agents are being used in applications where both the environment and the reasoning task are dynamically evolving. An agent's representation must also evolve to ensure its correctness and its suitability for the new problems it helps to solve;

— multi-agent cooperation and competition are becoming more common and the number of agents involved is increasing, e.g. on the Internet. Each of these agents may represent its knowledge of the environment differently, but the agents must communicate about the environment they share. There are too many different representations for all the possible alignments to be anticipated, especially when they change faster than they can be manually aligned; and

— the speed of agent interaction is increasing, e.g. in emergency response, so that manual repair or alignment is impractical. It must be automated, with provision for a human in the loop in some safety or security critical applications.

## Funding statement

This research was supported by EPSRC Platform Grant EP/J001058/1, EPSRC project EP/J020524/1 and ONR Global project N62909-12-1-7012.

## Author profile

**Alan Bundy** is Professor of Automated Reasoning in the School of Informatics at the University of Edinburgh. He is a fellow of several academic societies, including the Royal Society, the Royal Society of Edinburgh and the Royal Academy of Engineering. The major awards for his research, include the IJCAI Research Excellence Award (2007) and the CADE Herbrand Award (2007). He was awarded a CBE in 2012. He was Head of Informatics at Edinburgh (1998–2001) and a member of the Hewlett–Packard Research Board (1989–1991); the ITEC Foresight Panel (1994–1996), both the 2001 and 2008 Computer Science RAE panels (1999–2001, 2005–2008). He was the founding Convener of UKCRC (2000–2005) and a Vice President of the BCS (2010–2012). He is the author of over 250 publications.

## Acknowledgements

I thank my collaborators in the work surveyed here: Michael Chan, Jos Lehmann and Fiona McNeill. I also thank Andriana Gkaniatsou, Fiona McNeill, Boris Mitrovic and two anonymous referees for feedback on an earlier version.

## Footnotes

An invited Perspective to mark the election of Alan Bundy to the fellowship of the Royal Society in 2012.

↵1 ‘

*n*-ary’ is a generalization of unary, binary, ternary, etc., to mean having*n*arguments. A function's*arity*is the number of its arguments.↵3 Alternatively, factorization can be merged with binary resolution to give

*full resolution*, where unification is simultaneously used to unify one or more literals in each parent clause and then they are resolved together.↵4 See [3] for a discussion of how this error has arisen in practice.

↵5 Or we could use a more sophisticated representation of time.

↵6 This problem was originally posed by an American. In Britain, we would call it a chess board or draughts board.

↵7 The term ‘ontology’ is usually preferred over ‘logical theory’ in the field of software agents on the Internet.

↵8 The term ‘ontology’ is used to avoid confusion between logical and physical theories.

↵9 Of course, resolution, unification and skolem functions had not been invented when Cauchy produced this faulty proof. Our version of the faulty proof is a modern reconstruction. In fact, the diagnosis of such faulty proofs led to Frege's invention of first-order logic and thus, indirectly, to resolution, etc.

↵10 Actually, reformation also suggests removing the second argument from +, but we use heuristics to prune repairs to standard functions, such as +.

- Received March 25, 2013.
- Accepted June 4, 2013.

- © 2013 The Author(s) Published by the Royal Society. All rights reserved.