Automatic theory repair systems help identify and repair faults in a knowledge base, which has useful applications in artificial intelligence such as decision systems. The ABC system is a state-of-the-art implementation of such systems which combines three existing techniques: abduction, belief revision and conceptual change, but with a limitation that it only accepts Datalog logic. To enhance its expressive power, this study extends the ABC system to first-order logic (ABC_FOL), by augmenting the fault detection module and adding new repair plans to the system. The resultant extended system is able to correctly identify faults and generate sensible repairs across a diverse set of first-order logic examples that cannot be expressed in Datalog logic.
1. Introduction considering real-world scenarios, some complex rules (such as Government laws and regulations) simply cannot be encoded in Datalog logic. It is hence important to consider first-order logic (FOL), a more expressive logic that allows translation of almost any natural language statement to FOL statements [5]. This project aims to extend ABC to support FOL while retaining domainindependence. The hypothesis is that ABC techniques can be adapted to repair FOL theories, ofering some potential repairs, though not all of them.
Referring to figure 1, the project focuses on modifying C2 and C3 of ABC, as follows: 1. Developing an ABC theorem prover for FOL, generating partial proofs for repairs (C2). 2. Extending existing repair strategies to accommodate FOL (C3). 3. Creating new FOL-specific repair strategies (C3). 2. Extension of Fault Detection (C2) 2.1. Ancestor Resolution Ancestor resolution involves resolving the current clause with one of its own ancestors [6]. This concept is used in SL-resolution, where ancestors refer to intermediate goal clauses derived through resolution steps (RS). Incorporating ancestor resolution in FOL is essential due to its ability to handle non-Horn clauses, enabling new rules and theorems to emerge during the resolution process. This adaptability proves crucial in correctly deriving desired goals.
Consider the following example:
(, ℎ) =⇒ (, ). (, ) =⇒ (, ℎ).
=⇒ (, ) ∨ (, ℎ)
Figure 2 shows the inference result of (, ). The final resolution step, as highlighted in green, reuses the derivation result of the initial step (red) to prove the desired result. Without ancestor resolution, we would not be able to prove the result. (, ) =⇒ =⇒ (, ℎ) =⇒ (, ) 2.2. Occurs Check The occurs check is crucial for inference soundness, preventing cyclic substitutions where a variable is bound to a term containing itself, e.g., ( )/ [6]. Unlike the prior ABC version, the new FOL context introduces functions, rendering the occurs check necessary. This issue arises only when binding a variable to a function-containing a term, not a constant.
Consider the illustrative example:
(, ) ≡ (, ( )) The sign ≡ represents a unification problem. Here, unifying the second argument encounters the challenge ≡ ( ), causing the occurs check to fail due to cyclic substitution.
The project reinstates the occurs check into the unification algorithm. The condition ∈ () is verified within the case of the standard unification. Readers can refer to [ 6] for details of the occurs check. 3. Extension of Repair Generation (C3) A summary of old and new repair plans in ABC_FOL are listed in table 1, appendix A. The description of the changes are as follows. 3.1. Extension of ABC’s Framework ABC’s framework needs to be modified for FOL, including a new trace-back, incorporating functions, and removing restrictions of Datalog.
A repair is generated to block an unwanted unification or unblock a wanted unification in a resolution process, which has to modify a source axiom that is originally from the input theory rather than a theorem that is derived during resolution. Otherwise, the fault will still be derivable from the source axioms.
Thus, a trace-back algorithm is pivotal in pinpointing the source axiom for a targeted uniifcation from a proof. This necessity arises from ancestor resolution. The accurate change propagation to the pertinent axiom hinges on the trace-back process.
In order to incorporate functions, we adapted ABC’s framework to accept functions and be able to accurately identify constants, variables, predicates and functions.
Finally, a number of restrictions are modified in each specific old repair plan, that targets FOL’s distinction from Datalog - non-Horn clauses, allowing orphan variables (variables that are solely present in the head but not the body), predicates with function arguments. 3.2. New Repair Plans A brief summary of each of the repair plans is provided as follows. The first three fix an incompatibility that a proposition in the false set of preferred structure is derived so that we want to break a unification in its proof. The last is for an insuficiency that a proposition in the true set of the preferred structure cannot be derived, where we want to fix the failed unification to build a proof for it. Readers are directed to the project’s github repository [7] for a detailed description of the repair plans.
CR7-10: Break unification of a function : These repairs break unification of two functions by renaming functions, renaming constant arguments, weakening variables or adding diferent constants, which inherently breaks the predicate-level unification. The repair plans accommodate functions with various nesting depths.
CR11: Break 1(⃗) ≡ (⃗ ) by adding a variable to : This repair breaks unification by failing the occurs check, which is achieved by adding a variable that would cause cyclic substitution.
CR12: Break 1(⃗) ≡ (⃗ ) by adding an unprovable alternative (⃗): Appends an unprovable positive literal to the original axiom that satisfies certain conditions, efectively breaking the unification.
SR6: Fix the failed unification ̸= by removing all occurrences of a variable : Fixing a failed occurs check by removing all occurrences of the variable that leads to a cyclic substitution.
An example scenario that utilizes the new repair plans is a repair of an erroneous mathematical
equation. Consider the equation: ∃, ∀. ̸= . This equation can be formulated in ABC_FOL
in the following form: ¬(, ). This causes a contradiction with the fact (, ), which
is also added as an axiom in ABC_FOL. The new repair plan, CR11, is able to remedy this by
introducing a new variable to the constant , changing equation ¬(, ) to the following:
¬(, 1( ))
(
Note that 1 is a function yet to be assigned any meaning, as in any functions which
arise from skolemization. In many applications, we need to assign values to the new functions
for the logical system to behave correctly. Suppose that, based on other observations, a new
rule 1() = is added to the theory - this raises yet another contradiction with the
rule (
Now, CR7 is able to rename the function 1 in (
This makes sure the function in equation (
Passing this formulation to FOL_ABC, a total of 56 repair plans are generated, spanning the
use of various repair plans in repairing incompatibility. One of the solution uses the repair CR6
to add an unprovable precondition to (
¬ ( ) ∨ (, 1, 2) ∨ ( )
Given that the above formulation has no other reasonable candidates for the unprovable
precondition, the predicate is used. This could be linked to some specific mathematical
definitions that establish point as a vertex.
(
The extension is successfully integrated into the ABC codebase1. The evaluation of ABC_FOL supports the research hypothesis. The system generates numerous potential repairs to rectify identified faults while ensuring semantic coherence. ABC_FOL is poised for diverse applications 1Github Link: https://github.com/tpmmthomas/ABC_FOL in decision systems, law enforcement, and knowledge graphs, ofering broader usability than ABC_Datalog.
The project encountered several limitations, including the limited literature on automated theory repair techniques, inadequate data availability for FOL theorems, and evaluation constraints due to the subjective nature of repair output assessment. Future work suggestions include allowing non-ground assertions in PS to handle more complex statements, designing tailored heuristics for FOL theories to improve eficiency, exploring sorted logic extension for better proof search guidance, and conducting a more thorough evaluation of ABC_FOL.
A. Repair Plans Summary
S abT suA foa irva from R )
) − ty ( li →2 i
b a t ≡ a ) p
m − o ( c →1 I(n . ) :e −
( d i s →2 r e h ) it e ≢ . ′ : o ts t
n ta
s n − .
( ′ o →′1
e t a c i ed r o ) r o t le b a o i
r t r n p − av e
( r e →′2 e
n fie m ek
d )≢ ean ea d d . .
) n o c − ix 2 e l , b a v o m o ( →2 a e
h ≢ t e t ) 1 e l
e ≡ ≡ ) = ∧ = ( ∨ ) h c t a m s i m / h c t a t e g r a m 2
1 T ( . o t
) on . c 2 t le n , b e r ( fe 2 i d av ⃗ ia
r d ̸≡ d
d d ) A 1 n o i t c u d b
t e . u l ) b − li ( h c i h w e − l ( l l →1 a u e . →1 ) s e − v ( →1 ro p n o i t r e s s a m d r n t o te f e x R E . . 1 2 e r h
a t d d le d d A . .
m io in x a p a n i r a a v n f i g o i r s o ce m en o r r r f
u ) c c o ) = ∧ ( ) ∨ = ∧ = ( , 2 1 m n a a l
n P r i a p e R .
R 1 − .2
, W A . . 3
D 4 − .5 ( R →1 R R R ( →1 R
.
. 6 7 ⃗ 8 R R (1 R
A W . .
0 ,
2 . 1 9 1 ⃗ 1 1 R R (1 R R
A . e R C C C C C C C C C C C C R R R R R R S S S S S S =
= ∧
∧ = = = =
= ∨ ) ) =
=
∧ =
∧ 2
= = =
1 ( ( ) ) ⃗ ( ⃗ ( 1 2 =
≡ =
∧ = ) ) = ( ∨ (
=
= ≠ , 2 1 ) − ( →2 )
y ≢ c
n ) − ( →1 I(n e i ifc u s B. Definition of Eggtimer The , which is the target polygon to block, can be formalized by the set = {1, 2, 3, 4}, = {1, 2, 3, 4}, and the meeting points (1, 1, 2), (2, 2, 3), (3, 3, 4), (4, 4, 1), (, 1, 3). A graphical illustration is provided as follows.