$$ extsf ACUOS^mathbf 2$$ : A High-Performance System for Modular ACU Generalization with Subtyping and Inheritance

Generalization in order-sorted theories with any combination of associativity (A), commutativity (C), and unity (U) algebraic axioms is finitary. However, existing tools for computing generalizers (also called "anti-unifiers") of two typed structures in such theories do not currently scale to real size problems. This paper describes the ACUOS2 system that achieves high performance when computing a complete and minimal set of least general generalizations in these theories. We discuss how it can be used to address artificial intelligence (AI) problems that are representable as order-sorted ACU generalization, e.g., generalization in lists, trees, (multi-)sets, and typical hierarchical/structural relations. Experimental results are also given to demonstrate that ACUOS2 greatly outperforms the predecessor tool ACUOS by running up to five orders of magnitude faster.