The ABC system supports analogical abduction algorithms for knowledge transfer, e.g., existing logical rules are adapted, by reformation, into new rules by substituting symbols for similar ones. Although such knowledge transfer method can easily expand knowledge sets, it is likely to produce inconsistent knowledge, e.g., equations that do not fit target data in the real world. To solve this problem, we extend the classic reformation algorithm to repair numerical equations that violate target data. Equation reformation is achieved by weakening equation parameters when unblocking failed SLD-resolution proofs. The feasibility of numerical equation reformation is demonstrated by the automated repair of a faulty electrostatic force equation that is analogically transferred from the gravity equation.
Analogical reasoning is common in human thinking, ranging from knowledge acquisition and
language learning, to scientific problem solving and program design. For instance, the analogy
between natural and computational systems has led to various natural computing algorithms,
e.g., genetic algorithms [
Existing studies have focused on the formalism of analogical reasoning and theory repair. In the HDTP framework [10], analogies can be formalised by mapping terms from a source theory to a target theory. Such mappings can be applied to existing logical rules in the source theory, leading to new rules in the target theory. Apart from HDTP, faulty theories may be repaired using the reformation algorithm supported by the ABC theory repair system [11, 12, 13, 14, 15], which revises logical rules by enabling expected rule applications and disabling unexpected ones. However, as reformation uses the pure symbolic unification [ 16] that deals with predicates rather than numbers, numerical expressions may not be appropriately repaired.
In this work, we intend to develop a model that formalises human analogical reason. As there are many prior studies [17, 18, 10, 8] on how to compute analogy mappings, our work focuses on a post-processing algorithm that repairs faulty analogy mappings. We start from extending reformation to automate the repair of faulty numerical equations produced by human analogy, whereas the automation of the whole analogy process is considered as future work. Numerical equations are of great importance in natural science and engineering as they can be used to formalise data, simplify problems and make calculations. The integration of reformation and numerical computation is likely to expand the application of theory repair in real world problems. Although our approach is work-in-progress and not fully implemented, at the first stage, we have the following contributions: • The reformation algorithm is extended to repair numerical equations. • The algorithm is used to automatically repair an analogical blend of gravity and electrostatic force.
Analogous numerical equations are often used in our life. For instance, when shopping online, people may compare products by functionalities and prices, i.e., people use equations of costperformance ratio to score the products in mind. To compare two products, their information needs to be aligned, so that they can be scored by similar equations. Our earlier work [9] gives some insight on how to align two product models and use reformation to make the alignment consistent.
We will show that similar techniques can also be used to develop a physical theory of a new domain from one for an old domain. For instance, in electrical engineering, power flows are considered similar to water flows, so that many equations, e.g., those of potential energy, work and wave, can be adapted to model both power grids and hydropower systems. The correctness of the adapted equations is judged using real-world data. Due to combinatorial explosions, adapting and judging equations is time-consuming for humans. We use reformation to automate the process.
We extend reformation [13] to equational reasoning by introducing a numerical constraint solver, e.g., the Z3 solver [19], into the unblocking function. During SLD-resolution [20], unblocking can repair faulty definite clauses by enabling wanted unifications, i.e., if the unification of two compound terms ( 1, … , ) and ( 1, … , ) fails, minimal changes will be applied to the terms or their sub-terms to achieve a successful unification. If the terms can be numerically evaluated, then the equation ( 1, … , ) = ( 1, … , ) can be solved using the Z3 solver. If the solver fails, then the equation will be weakened by various repair operators, such as replacing constants with unknowns and introducing new functions with unknowns. The weakened equations can be solved by the solver to determine the values of unknowns. By replacing the original equation with the weakened equation, the unification becomes successful.
The proposed approach is implemented as a resolution module and an equation repair module.1 The resolution module, based on SWI-Prolog [21], can recursively resolve goal problems into sub-problems by user-specified rules until no rules can be applied. The equation repair module, based on Z3 [19] and Python [22], can try to solve equations in the sub-problems and repair unsolvable equations. The suggested repairs are applied to the user-specified rules, resulting in a set of updated rules that will be checked by the resolution module. With the implementation, we suggest the following steps to achieve equation transfer and repair. 1. A source theory and a set of analogical relations are provided by humans to obtain a blended theory. 2. A set of target data is provided by humans to verify the blended theory. 3. If any target data results in failed proofs, then reformation is used to unblock the proofs, which causes any equations violating the target data to be repaired.
Gravity and electrostatic force seem to be analogous as both of them act on objects without actual contact. Gravity is subject to masses and positions of objects, whereas electrostatic force is subject to charges and positions of objects. However, gravity only attracts objects, whereas electrostatic force can either attract or repel objects. The following process shows how to use reformation to adapt Newton’s equation of gravity to Coulomb’s equation of electrostatic force. Given the equation of gravity as the source theory: 1, 1) ∧ ( 1, 2) = 1, 1, 1, 1) ∧ ( 2, 2) ∧ ( 2, 2, 2, 2) ⟹ 6.67 × 10−11 ⋅ 1 ⋅ 2 ( 2 − 1, 2 − 1, 2 − 1) ⏟(⏟⏟⏟2⏟−⏟⏟⏟⏟⏟1⏟)⏟2⏟⏟+⏟⏟(⏟⏟⏟2⏟⏟−⏟⏟⏟⏟1⏟)⏟2⏟⏟+⏟⏟⏟(⏟⏟2⏟⏟−⏟⏟⏟⏟1⏟)2 ⋅ ⏟√⏟⏟(⏟⏟⏟2⏟−⏟⏟⏟⏟⏟1⏟)⏟2⏟⏟+⏟⏟(⏟⏟⏟2⏟⏟−⏟⏟⏟⏟1⏟)⏟2⏟⏟+⏟⏟⏟(⏟⏟2⏟⏟−⏟⏟⏟⏟1⏟)2
Magnitude Direction ℎ (, ) means that a point-like object has charges . ( 1, 2) is the electrostatic force that a charged object 2 acts on another charged object 1. The blended theory is expected to prove a goal that represents target data: ℎ( ( 1, 4 × 10−8) ∧ ( 2, 0, 0, 0) ⟹ ( 1, 0.1, 0, 0) ∧ ℎ( 2, 4 × 10−8) ∧
1, 2) = (1.4384 × 10−3, 0, 0) 1The source code is available via https://github.com/cchrewrite/Numerical-Equation-Repair. (, ) means that a point-like object has mass . (, , , ) means that the coordinate of the object in a 3D space is (, , ) . ( 1, 2) is the gravity that an object 2 acts on another object 1, which is a 3D vector with a magnitude and a direction. By analogical relations ↦ ℎ and ↦ , a blended theory can be obtained: 1, 1) ∧ ( 1, 1, 1, 1) ∧ ℎ( 2, 2) ∧ ( 2, 2, 2, 2) ⟹ 6.67 × 10−11 ⋅ 1 ⋅ 2 ( 2 − 1, 2 − 1, 2 − 1) 1, 2) = ( 2 − 1)2 + ( 2 − 1)2 + ( 2 − 1)2 ⋅ √( 2 − 1)2 + ( 2 − 1)2 + ( 2 − 1)2 ( ( During the resolution to the goal, the equation ( 1, 2) = (1.4384 × 10−3, 0, 0) fails. To weaken the equation, the constant 6.67 × 10−11 is replaced with an unknown and solved by the constraint solver, leading to the following repaired theory with = −8.99 × 10 9: The repaired theory fits Coulomb’s equation of electrostatic force as the revised parameter −8.99 × 109 fits Coulomb’s constant ( ≈ 8.99 × 109), which means that the equation transfer is successful. The parameter is negative because charges are signed, i.e., positive charges attract negative charges and repel positive charges, and vice versa.
We have demonstrated the feasibility for using reformation to repair numerical equations in analogical blends, i.e., a failed unification with equations may be unblocked by weakening the equations. This approach can repair a wide range of equations if they meet three requirements: 1. all variables in the equations can be instantiated by SLD-resolution and user-specified rules, 2. all operators in the equations are supported by the constraint solver, and 3. the equations can be made true by finding alternative constants.
As the capability of equation repair is limited by constraint solvers, satisfiability of equations, etc., we may introduce symbolic constraint solvers and explore how to generally repair equations in larger theories in the future. Additionally, combining with analogy mapping algorithms, our approach will have potential applications in scientific knowledge discovery. In other words, equations describing the characteristics of an object, e.g., a material, a species and a (natural or social) phenomenon, can be transferred to describe another similar object. Our approach might be used to automatically repair some transferred equations that violate real-world data, so that the eficiency of research can be improved.
For the purpose of open access, the author has applied a Creative Commons Attribution (CC BY) licence to any Author Accepted Manuscript version arising from this submission. [3] A. R. Jordehi, J. Jasni, Parameter selection in particle swarm optimisation: a survey, Journal of Experimental and Theoretical Artificial Intelligence 25 (2013) 527–542. doi: 1 0 . 1 0 8 0 / 0 9 5 2 8 1 3 X . 2 0 1 3 . 7 8 2 3 4 8 . [4] K. J. Holyoak, K. Koh, Surface and structural similarity in analogical transfer, Memory and Cognition 15 (1987) 332–340. doi:1 0 . 3 7 5 8 / B F 0 3 1 9 7 0 3 5 . [5] L. Eliot, Analogical problem-solving and expert systems, IEEE Expert 1 (1986) 17–28.
doi:1 0 . 1 1 0 9 / M E X . 1 9 8 6 . 4 3 0 6 9 5 1 . [6] M. Eppe, E. Maclean, R. Confalonieri, O. Kutz, M. Schorlemmer, E. Plaza, K. Kühnberger, A computational framework for conceptual blending, Artificial Intelligence 256 (2018) 105–129. doi:1 0 . 1 0 1 6 / j . a r t i n t . 2 0 1 7 . 1 1 . 0 0 5 . [7] T. Liang, Analogical reasoning and case-based learning in model management systems,
Decision Support Systems 10 (1993) 137–160. doi:1 0 . 1 0 1 6 / 0 1 6 7 - 9 2 3 6 ( 9 3 ) 9 0 0 3 5 - 2 . [8] T. R. Hinrichs, K. D. Forbus, Transfer learning through analogy in games, AI Magazine 32 (2011) 70–83. doi:1 0 . 1 6 0 9 / a i m a g . v 3 2 i 1 . 2 3 3 2 . [9] A. Bundy, E. Maclean, The use of reformation to repair faulty analogical blends, in: the 5th UK Ontology Network, Newcastle upon Tyne, UK, April 14, 2016. [10] H. Gust, K. Kühnberger, U. Schmid, Metaphors and heuristic-driven theory projection (HDTP), Theoretical Computer Science 354 (2006) 98–117. doi:1 0 . 1 0 1 6 / j . t c s . 2 0 0 5 . 1 1 . 0 0 9 . [11] X. Li, Automating the repair of faulty logical theories, Doctoral Dissertation, the University of Edinburgh (2021). [12] M. Urbonas, A. Bundy, J. Casanova, X. Li, The use of MAX-SAT for optimal choice of automated theory repairs, in: Proceedings of the 40th SGAI International Conference on Artificial Intelligence, Cambridge, UK, December 15-17, 2020, pp. 49–63. doi: 1 0 . 1 0 0 7 / 9 7 8 - 3 - 0 3 0 - 6 3 7 9 9 - 6 _ 4 . [13] A. Bundy, B. Mitrovic, Reformation: A domain-independent algorithm for theory repair,
Technical report, the University of Edinburgh (2016). [14] C. Cai, The application of reformation to repair faulty analogical blends, MSc Dissertation, the University of Edinburgh (2016). [15] X. Li, A. Bundy, A. Smaill, ABC repair system for Datalog-like theories, in: Proceedings of the 10th International Joint Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management, Seville, Spain, September 18-20, 2018, pp. 333–340. doi:1 0 . 5 2 2 0 / 0 0 0 6 9 5 9 7 0 3 3 3 0 3 4 0 . [16] J. H. Siekmann, Unification theory, Journal of Symbolic Computation 7 (1989) 207–274.
doi:1 0 . 1 0 1 6 / S 0 7 4 7 - 7 1 7 1 ( 8 9 ) 8 0 0 1 2 - 4 . [17] D. Gentner, Structure-mapping: A theoretical framework for analogy, Cognitive Science 7 (1983) 155–170. doi:1 0 . 1 2 0 7 / s 1 5 5 1 6 7 0 9 c o g 0 7 0 2 _ 3 . [18] B. Falkenhainer, K. D. Forbus, D. Gentner, The structure-mapping engine: Algorithm and examples, Artificial Intelligence 41 (1989) 1–63. doi: 1 0 . 1 0 1 6 / 0 0 0 4 - 3 7 0 2 ( 8 9 ) 9 0 0 7 7 - 5 . [19] L. M. de Moura, N. S. Bjørner, Z3: an eficient SMT solver, in: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, Hungary, March 29-April 6, 2008, pp. 337–340. doi:1 0 . 1 0 0 7 / 9 7 8 - 3 - 5 4 0 - 7 8 8 0 0 - 3 _ 2 4 . [20] R. A. Kowalski, D. Kuehner, Linear resolution with selection function, Artificial Intelligence 2 (1971) 227–260. doi:1 0 . 1 0 1 6 / 0 0 0 4 - 3 7 0 2 ( 7 1 ) 9 0 0 1 2 - 9 . [21] J. Wielemaker, T. Schrijvers, M. Triska, T. Lager, SWI-prolog, Theory and Practice of Logic
Programming 12 (2012) 67–96. doi:1 0 . 1 0 1 7 / S 1 4 7 1 0 6 8 4 1 1 0 0 0 4 9 4 . [22] G. Van Rossum, F. L. Drake Jr, Python Tutorial, Python Software Foundation, 2012.