In this paper we demonstrate how logic programming systems and Automated first- order logic Theorem Provers (ATPs) can improve the accuracy of Large Language Models (LLMs) for logical reasoning tasks where the baseline performance is given by direct LLM solutions. We first evaluate LLM reasoning on steamroller problems using the PRON- TOQA benchmark. We show how accuracy can be improved with a neuro-symbolic ar- chitecture where the LLM acts solely as a front-end for translating a given problem into a formal logic language and an automated reasoning engine is called for solving it. How- ever, this approach critically hinges on the correctness of the LLM translation. To assess this translation correctness, we secondly define a framework of syntactic and semantic er- ror categories. We implemented the framework and used it to identify errors that LLMs make in the benchmark domain. Based on these findings, we thirdly extended our method with capabilities for automatically correcting syntactic and semantic errors. For semantic error correction we integrate first-order logic ATPs, which is our main and novel contribu- tion. We demonstrate that this approach reduces semantic errors significantly and further increases the accurracy of LLM logical reasoning.

Abstract FOLD-RM is an explainable machine learning classification algorithm that uses training data to create a set of classification rules. In this paper, we introduce CON-FOLD which extends FOLD-RM in several ways. CON-FOLD assigns probability-based confidence scores to rules learned for a classification task. This allows users to know how confident they should be in a prediction made by the model. We present a confidence-based pruning algorithm that uses the unique structure of FOLD-RM rules to efficiently prune rules and prevent overfitting. Furthermore, CON-FOLD enables the user to provide preexisting knowledge in the form of logic program rules that are either (fixed) background knowledge or (modifiable) initial rule candidates. The paper describes our method in detail and reports on practical experiments. We demonstrate the performance of the algorithm on benchmark datasets from the UCI Machine Learning Repository. For that, we introduce a new metric, Inverse Brier Score, to evaluate the accuracy of the produced confidence scores. Finally, we apply this extension to a real-world example that requires explainability: marking of student responses to a short answer question from the Australian Physics Olympiad.

Abstract Fusemate is a logic programming system that implements the possible model semantics for disjunctive logic programs. Its input language is centered around a weak notion of stratification with comprehension and aggregation operators on top of it. Fusemate is implemented as a shallow embedding in the Scala programming language. This enables using Scala data types natively as terms, a tight interface with external systems, and it makes model computation available as an ordinary container data structure constructor. The paper describes the above features and implementation aspects. It also demonstrates them with a non-trivial use-case, the embedding of the description logic $$\mathcal ALCIF$$ A L C I F into Fusemate’s input language.

Model generation is a problem complementary to theorem proving and is important for fault analysis and debugging of formal specifications of security protocols, programs and terminological definitions, for example. This paper discusses several ways of enhancing the paradigm of bottom-up model generation, with the two main contributions being a new range-restriction transformation and generalized blocking techniques. The range-restriction transformation refines existing transformations to range-restricted clauses by carefully limiting the creation of domain terms. The blocking techniques are based on simple transformations of the input set together with standard equality reasoning and redundancy elimination techniques, and allow for finding small, finite models. All possible combinations of the introduced techniques and a classical range-restriction technique were tested on the clausal problems of the TPTP Version 6.0.0 with an implementation based on the SPASS theorem prover using a hyperresolution-like refinement. Unrestricted domain blocking gave best results for satisfiable problems, showing that it is an indispensable technique for bottom-up model generation methods, that yields good results in combination with both new and classical range-restricting transformations. Limiting the creation of terms during the inference process by using the new range-restricting transformation has paid off, especially when using it together with a shifting transformation. The experimental results also show that classical range restriction with unrestricted blocking provides a useful complementary method. Overall, the results show bottom-up model generation methods are good for disproving theorems and generating models for satisfiable problems, but less efficient for unsatisfiable problems.

In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this article we show how to integrate a modern treatment of equality in the hyper tableau calculus. It is based on splitting of positive clauses and an adapted version of the superposition inference rule, where equations used for superposition are drawn (only) from a set of positive unit clauses, and superposition inferences into positive literals is restricted into (positive) unit clauses only. The calculus also features a generic, semantically justified simplification rule which covers many redundancy elimination techniques known from superposition theorem proving. Our main results are soundness and completeness of the calculus, but we also show how to apply the calculus for finite model computation, and we briefly describe the implementation.