Property Invariant Embedding for Automated Reasoning

27 November 2019

Papers citing "Property Invariant Embedding for Automated Reasoning"

26 / 26 papers shown

Title
Efficient Neural Clause-Selection Reinforcement Martin Suda 97 0 0 10 Mar 2025
Solving Hard Mizar Problems with Instantiation and Strategy Invention Jan Jakubuv Mikoláš Janota Josef Urban 66 0 0 25 Jun 2024
A Survey on Deep Learning for Theorem Proving Zhaoyu Li Jialiang Sun Logan Murphy Qidong Su Zenan Li Xian Zhang Kaiyu Yang Xujie Si LRM 123 32 0 15 Apr 2024
Learning Guided Automated Reasoning: A Brief Survey Lasse Blaauwbroek David M. Cerna Thibault Gauthier Jan Jakubruv C. Kaliszyk Martin Suda Josef Urban LRM 93 5 0 06 Mar 2024
gym-saturation: Gymnasium environments for saturation provers (System description) Boris Shminke 71 1 0 16 Sep 2023
An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations Achille Fokoue Ibrahim Abdelaziz Mayank Agarwal S. Ikbal Akihiro Kishimoto Guilherme Lima Ndivhuwo Makondo Radu Marinescu OOD NAI 49 5 0 15 May 2023
MizAR 60 for Mizar 50 Jan Jakubruv Karel Chvalovský Z. Goertzel C. Kaliszyk Mirek Olvsák Bartosz Piotrowski S. Schulz Martin Suda Josef Urban 82 13 0 12 Mar 2023
Machine Learning Meets The Herbrand Universe Jelle Piepenbrock Josef Urban Konstantin Korovin Miroslav Olvsák Tom Heskes Mikolávs Janota NAI 55 3 0 07 Oct 2022
Exploring Representation of Horn Clauses using GNNs (Extended Technical Report) Chencheng Liang P. Rümmer Marc Brockschmidt 72 1 0 14 Jun 2022
The Isabelle ENIGMA Z. Goertzel Jan Jakubruv C. Kaliszyk Miroslav Olvsák Jelle Piepenbrock Josef Urban AIMat 44 13 0 04 May 2022
Adversarial Learning to Reason in an Arbitrary Logic Stanislaw J. Purgal C. Kaliszyk 64 1 0 06 Apr 2022
Learning Theorem Proving Components Karel Chvalovský Jan Jakubuv Miroslav Olsák Josef Urban LRM 51 8 0 21 Jul 2021
Fast and Slow Enigmas and Parental Guidance Z. Goertzel Karel Chvalovský Jan Jakubuv Miroslav Olsák Josef Urban 78 11 0 14 Jul 2021
Learning to Guide a Saturation-Based Theorem Prover Ibrahim Abdelaziz Mayank Agarwal B. Makni Vernon Austil Cristina Cornelio ... Pavan Kapanipathi Ndivhuwo Makondo Kavitha Srinivas Michael Witbrock Achille Fokoue 54 17 0 07 Jun 2021
The Role of Entropy in Guiding a Connection Prover Zsolt Zombori Josef Urban Miroslav Olsák 64 11 0 31 May 2021
Improving ENIGMA-Style Clause Selection While Learning From History Martin Suda 45 1 0 26 Feb 2021
Neural Termination Analysis Mirco Giacobbe Daniel Kroening Julian Parsert 81 17 0 07 Feb 2021
A Study of Continuous Vector Representationsfor Theorem Proving Stanislaw J. Purgal Julian Parsert C. Kaliszyk NAI 51 5 0 22 Jan 2021
Prolog Technology Reinforcement Learning Prover Zsolt Zombori Josef Urban C. Brown OffRL 58 14 0 15 Apr 2020
Tactic Learning and Proving for the Coq Proof Assistant Lasse Blaauwbroek Josef Urban H. Geuvers 114 24 0 20 Mar 2020
Stateful Premise Selection by Recurrent Neural Networks Bartosz Piotrowski Josef Urban LRM 54 21 0 11 Mar 2020
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) Jan Jakubuv Karel Chvalovský Miroslav Olsák Bartosz Piotrowski Martin Suda Josef Urban 65 44 0 13 Feb 2020
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic Ibrahim Abdelaziz Veronika Thost Mayank Agarwal Achille Fokoue 61 6 0 02 Feb 2020
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling Mayank Agarwal Ibrahim Abdelaziz Cristina Cornelio Veronika Thost Lingfei Wu Kenneth D. Forbus Achille Fokoue NAI AI4CE GNN 174 36 0 15 Nov 2019
A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving Mayank Agarwal Ibrahim Abdelaziz B. Makni Spencer Whitehead Cristina Cornelio Pavan Kapanipathi Kavitha Srinivas Veronika Thost Michael Witbrock Achille Fokoue LRM 83 10 0 05 Nov 2019
Towards Finding Longer Proofs Zsolt Zombori Adrián Csiszárik Henryk Michalewski C. Kaliszyk Josef Urban OffRL LRM 83 16 0 30 May 2019