Unification is one of the fundamental operations in automated first-order reasoning and is used intensively in fields such as theorem proving and logic programming. Since Robinson’s pioneering proposal, several efficient algorithms based on sophisticated data structures have been developed, and some approaches to its parallelization have been analyzed. Recent advances in hardware, particularly the rise of Graphical Processing Units (GPUs), give us the opportunity to work with large volumes of data in parallel. The use of GPUs is becoming increasingly common in applications beyond computer graphics, thanks to their massive parallelism, high memory bandwidth, and throughput-oriented architecture. However, these advantages are best leveraged when working with data structures that exhibit high regularity, such as dense arrays or matrices. Unfortunately, inductively defined expressions, commonly used in unification, typically exhibit irregular and sparse structures, making them unsuitable for direct GPU acceleration. In this work, we present a new approach to efficiently unify large batches of terms by introducing a novel matrix-based representation that avoids the irregularities inherent in traditional approaches. We have implemented a C-based prototype that achieves competitive performance compared to a Prolog baseline, while also revealing how structural characteristics of the representation influence efficiency. This prototype provides the foundation for a massively parallel GPU-based unification engine, which we plan to develop in future work.

Although large language models (LLMs) have apparently acquired a certain level of grammatical knowledge and the ability to make generalizations, they fail to interpret negation, a crucial step in Natural Language Processing.We try to clarify the reasons for the sub-optimal performance of LLMs understanding negation.We introduce a large semi-automatically generated dataset of circa 400,000 descriptive sentences about commonsense knowledge that can be true or false in which negation is present in about 2/3 of the corpus in different forms.We have used our dataset with the largest available open LLMs in a zero-shot approach to grasp their generalization and inference capability and we have also fine-tuned some of the models to assess whether the understanding of negation can be trained.Our findings show that, while LLMs are proficient at classifying affirmative sentences, they struggle with negative sentences and lack a deep understanding of negation, often relying on superficial cues.Although finetuning the models on negative sentences improves their performance, the lack of generalization in handling negation is persistent, highlighting the ongoing challenges of LLMs regarding negation understanding and generalization.The dataset and code are publicly available: https://github.com/hitz-zentroa/ This-is-not-a-Dataset

In this paper, we analyse and compare several correction methods of knowledge resources with the purpose of improving the abilities of systems that require commonsense reasoning with the least possible human-effort.To this end, we cross-check the WordNet meronymy relation member against the knowledge encoded in a SUMO-based first-order logic ontology on the basis of the mapping between WordNet and SUMO.In particular, we focus on the knowledge in WordNet regarding the taxonomy of animals and plants.Despite being created manually, these knowledge resources -WordNet, SUMO and their mapping-are not free of errors and discrepancies.Thus, we propose three correction methods by semi-automatically improving the alignment between WordNet and SUMO, by performing some few corrections in SUMO and by combining the above two strategies.The evaluation of each method includes the required human-effort and the achieved improvement on unseen data from the WebChild project, that is tested using first-order logic automated theorem provers.

Most commonly, the Open World Assumption is adopted as a standard strategy for the design, construction and use of ontologies. This strategy limits the inferencing capabilities of any system because non-asserted statements (missing knowledge) could be assumed to be alternatively true or false. As we will demonstrate, this is especially the case of first-order logic (FOL) ontologies where non-asserted statements is nowadays one of the main obstacles to its practical application in automated commonsense reasoning tasks. In this paper, we investigate the application of the Closed World Assumption (CWA) to enable a better exploitation of FOL ontologies by using state-of-the-art automated theorem provers. To that end, we explore different CWA formulations for the structural knowledge encoded in a FOL translation of the SUMO ontology, discovering that almost 30 % of the structural knowledge is missing. We evaluate these formulations on a practical experimentation using a very large commonsense benchmark obtained from WordNet through its mapping to SUMO. The results show that the competency of the ontology improves more than 50 % when reasoning under the CWA. Thus, applying the CWA automatically to FOL ontologies reduces their ambiguity and more commonsense questions can be answered

We describe a detailed analysis of a sample of large benchmark of commonsense reasoning problems that has been automatically obtained from WordNet, SUMO and their mapping.The objective is to provide a better assessment of the quality of both the benchmark and the involved knowledge resources for advanced commonsense reasoning tasks.By means of this analysis, we are able to detect some knowledge misalignments, mapping errors and lack of knowledge and resources.Our final objective is the extraction of some guidelines towards a better exploitation of this commonsense knowledge framework by the improvement of the included resources.

Formal ontologies are axiomatizations in a logic-based formalism. The development of formal ontologies is generating considerable research on the use of automated reasoning techniques and tools that help in ontology engineering. One of the main aims is to refine and to improve axiomatizations for enabling automated reasoning tools to efficiently infer reliable information. Defects in the axiomatization cannot only cause wrong inferences, but can also hinder the inference of expected information, either by increasing the computational cost of or even preventing the inference. In this paper, we introduce a novel, fully automatic white-box testing framework for first-order logic (FOL) ontologies. Our methodology is based on the detection of inference-based redundancies in the given axiomatization. The application of the proposed testing method is fully automatic since (i) the automated generation of tests is guided only by the syntax of axioms and (ii) the evaluation of tests is performed by automated theorem provers (ATPs). Our proposal enables the detection of defects and serves to certify the grade of suitability—for reasoning purposes—of every axiom. We formally define the set of tests that are (automatically) generated from any axiom and prove that every test is logically related to redundancies in the axiom from which the test has been generated. We have implemented our method and used this implementation to automatically detect several non-trivial defects that were hidden in various FOL ontologies. Throughout the paper we provide illustrative examples of these defects, explain how they were found and how each proof—given by an ATP—provides useful hints on the nature of each defect. Additionally, by correcting all the detected defects, we have obtained an improved version of one of the tested ontologies: Adimen-SUMO.

We describe the practical application of a black-box testing methodology for the validation of the knowledge encoded in WordNet, SUMO and their mapping by using automated theorem provers.In this paper, we concentrate on the part-whole information provided by WordNet and create a large set of tests on the basis of few question patterns.From our preliminary evaluation results, we report on some of the detected inconsistencies.

We introduce a new framework to evaluate and improve first-order (FO) ontologies using automated theorem provers (ATPs) on the basis of competency questions (CQs). Our framework includes both the adaptation of a methodology for evaluating ontologies to the framework of first-order logic and a new set of non-trivial CQs designed to evaluate FO versions of SUMO, which significantly extends the very small set of CQs proposed in the literature. Most of these new CQs have been automatically generated from a small set of patterns and the mapping of WordNet to SUMO. Applying our framework, we demonstrate that Adimen-SUMO v2.2 outperforms TPTP-SUMO. In addition, using the feedback provided by ATPs we have set an improved version of Adimen-SUMO (v2.4). This new version outperforms the previous ones in terms of competency. For instance, "Humans can reason" is automatically inferred from Adimen-SUMO v2.4, while it is neither deducible from TPTP-SUMO nor Adimen-SUMO v2.2.

We report on the results of evaluating the competency of a first-order ontology for its use with automated theorem provers (ATPs). The evaluation follows the adaptation of the methodology based on competency questions (CQs) [4] to the framework of first-order logic, which is presented in [2], and is applied to Adimen-SUMO [1]. The set of CQs used for this evaluation has been automatically generated from a small set of semantic patterns and the mapping of WordNet to SUMO. Analysing the results, we can conclude that it is feasible to use ATPs for working with Adimen-SUMO v2.4, enabling the resolution of goals by means of performing non-trivial inferences.

In this paper, the authors present Adimen-SUMO, an operational ontology to be used by first-order theorem provers in intelligent systems that require sophisticated reasoning capabilities (e.g. Natural Language Processing, Knowledge Engineering, Semantic Web infrastructure, etc.). Adimen-SUMO has been obtained by automatically translating around 88% of the original axioms of SUMO (Suggested Upper Merged Ontology). Their main interest is to present in a practical way the advantages of using first-order theorem provers during the design and development of first-order ontologies. First-order theorem provers are applied as inference engines for reengineering a large and complex ontology in order to allow for formal reasoning. In particular, the authors’ study focuses on providing first-order reasoning support to SUMO. During the process, they detect, explain and repair several important design flaws and problems of the SUMO axiomatization. As a by-product, they also provide general design decisions and good practices for creating operational first-order ontologies of any kind.