Related papers: Update report: LEO-II version 1.5
The automated theorem prover Leo-III for classical higher-order logic with Henkin semantics and choice is presented. Leo-III is based on extensional higher-order paramodulation and accepts every common TPTP dialect (FOF, TFF, THF),…
Leo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate…
A converter from first-order modal logics to classical higher- order logic is presented. This tool enables the application of off-the-shelf higher-order theorem provers and model finders for reasoning within first- order modal logics. The…
We introduce a new theorem prover for classical higher-order logic named auto2. The prover is designed to make use of human-specified heuristics when searching for proofs. The core algorithm is a best-first search through the space of…
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…
Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP). Deriving the most appropriate subsequent…
Discovering improved policy optimization algorithms for language models remains a costly manual process requiring repeated mechanism-level modification and validation. Unlike simple combinatorial code search, this problem requires searching…
Formal verification via theorem proving enables the expressive specification and rigorous proof of software correctness, but it is difficult to scale due to the significant manual effort and expertise required. While Large Language Models…
Recent advances in large language models (LLMs) have greatly improved their reasoning and decision-making abilities when deployed as agents. Richer reasoning, however, often comes at the cost of longer chain of thought (CoT), hampering…
Recent advances in large language models (LLMs) have made it increasingly difficult to distinguish human-written text from AI-generated content. Many existing detectors train supervised neural classifiers that achieve strong in-distribution…
This volume contains a selection of papers presented at the 17th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2022). The workshops are the premier technical forum for presenting research and experiences…
Garg and Abadi recently proved that prominent access control logics can be translated in a sound and complete way into modal logic S4. We have previously outlined how normal multimodal logics, including monomodal logics K and S4, can be…
PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. It includes a versatile formula macro system and supports the creation of documents that intersperse macro definitions, reasoner invocations and…
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of the ENIGMA guidance…
This volume contains the proceedings of the Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, ACL2 2015, a two-day workshop held in Austin, Texas, USA, on October 1-2, 2015. ACL2 workshops occur at…
Undergraduate students of artificial intelligence often struggle with representing knowledge as logical sentences. This is a skill that seems to require extensive practice to obtain, suggesting a teaching strategy that involves the…
This volume contains the proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications, held on May 30 and 31, 2013, in Laramie, Wyoming, USA. ACL2 is an industrial-strength automated reasoning system,…
The energy upgrade at LEP allows new regimes to be explored in the search for physics beyond the Standard Model. The searches for new physics using the ALEPH, DELPHI, L3, and OPAL data are described, and the results are presented.
This volume contains a selection of papers presented at the 16th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-2020). The workshops are the premier technical forum for presenting research and experiences…
Despite the success of large language models (LLMs), the task of theorem proving still remains one of the hardest reasoning tasks that is far from being fully solved. Prior methods using language models have demonstrated promising results,…