Lemmas: Generation, Selection, Application
Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.
Code (1)
Tasks
Automated Theorem ProvingSimilar Papers 제목 키워드 기반
Sense Contextualization in a Dependency-Based Compositional Distributional Model
Little attention has been paid to distributional compositional methods which employ syntactically structured vector models. As word vectors belonging to different syntactic categories have incompatible syntactic distribu…
LEMMARepresentation LearningSemantic CompositionWord Sense DisambiguationQabas: An Open-Source Arabic Lexicographic Database
We present Qabas, a novel open-source Arabic lexicon designed for NLP applications. The novelty of Qabas lies in its synthesis of 110 lexicons. Specifically, Qabas lexical entries (lemmas) are assembled by linking lemmas…
A model for prohibition and obligation dilemmas generation in virtual environments
Under the project Maccoy Critical, we would like to train individuals, in virtual environments, to handle critical situations such as dilemmas. These latter refer to situations where there is no ``good'' solution. In oth…
Partner Selection for the Emergence of Cooperation in Multi-Agent Systems Using Reinforcement Learning
Social dilemmas have been widely studied to explain how humans are able to cooperate in society. Considerable effort has been invested in designing artificial agents for social dilemmas that incorporate explicit agent mo…
Multi-agent Reinforcement LearningReinforcement LearningDAG: Dictionary-Augmented Generation for Disambiguation of Sentences in Endangered Uralic Languages using ChatGPT
We showcase that ChatGPT can be used to disambiguate lemmas in two endangered languages ChatGPT is not proficient in, namely Erzya and Skolt Sami. We augment our prompt by providing dictionary translations of the candida…