Keyword:automated theorem proving

Publications
Sorting Without Sorts Pamina Georgiou, Marton Hajdu and Laura Kovacs EasyChair Preprint 10632
Lazy and Eager Patterns in High-Performance Automated Theorem Proving Stephan Schulz EasyChair Preprint 10510
Model Based Interpolation for Uninterpreted Functions and Integer Linear Arithmetic Nikolaj Bjorner, Arie Gurfinkel, Sharon Shoham and Yakir Vizel EasyChair Preprint 10000
Goéland: a Concurrent Tableau-Based Theorem Prover (System Description) Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard and Hinde Bouziane EasyChair Preprint 8676
A Multithreaded Vampire with Shared Persistent Grounding Michael Rawson and Giles Reger EasyChair Preprint 5855
E 2.4 User Manual Stephan Schulz EasyChair Preprint 2272
A FOOLish Encoding of the Next State Relations of Imperative Programs Evgenii Kotelnikov, Laura Kovács and Andrei Voronkov EasyChair Preprint 98
E 2.0 User Manual Stephan Schulz EasyChair Preprint 8
Benchmarking LLMs Against TPTP: A Vision for the Near Future Andrija Urošević, Gordan Đurić and Sana Stojanović-Đurđević In:Proceedings of 16th International Workshop on the Implementation on Logics. Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (short papers)
Some Experiments with Twee-Style Goal-Directedness Stephan Schulz In:Proceedings of 16th International Workshop on the Implementation on Logics. Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (short papers)
Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop Theodore Kim and Adam Pease In:Proceedings of 16th International Workshop on the Implementation on Logics. Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (short papers)
Building Blocks for Reasoning on the BEAM Johannes Schuster and Christoph Benzmüller In:Proceedings of 16th International Workshop on the Implementation on Logics. Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (short papers)
Representation Abstraction and Proof Search for English-to-Logic Question Answering Tanel Tammet In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic Melanie Taprogge, Frédéric Blanqui and Alexander Steen In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Reasoning About Hyperproperties with Automated Theorem Provers Tobias Nießen, Ana Oliveira da Costa, Johannes Schoisswohl, Thomas A. Henzinger and Laura Kovács In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning
Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery Kristina Aleksandrova, Jan Jakubuv and Cezary Kaliszyk In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
A Generic Deskolemization Strategy Johann Rosain, Richard Bonichon, Julie Cailler and Olivier Hermant In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Waste Reduction: Experiments in Sharing Clauses between Runs of a Portfolio of Strategies (Experimental Paper) Tanel Tammet In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Saturating Sorting without Sorts Pamina Georgiou, Marton Hajdu and Laura Kovács In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Automated Theorem Provers Help Improve Large Language Model Reasoning Lachlan McGinness and Peter Baumgartner In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Automated Theorem Proving for Prolog Verification Fred Mesnard, Thierry Marianne and Etienne Payet In:LPAR 2024 Complementary Volume
Lazy and Eager Patterns in High-Performance Automated Theorem Proving Stephan Schulz In:Proceedings of the 7th and 8th Vampire Workshop
Refining Unification with Abstraction Ahmed Bhayat, Konstantin Korovin, Laura Kovacs and Johannes Schoisswohl In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
How Much Should This Symbol Weigh? A GNN-Advised Clause Selection Filip Bártek and Martin Suda In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Stateful Premise Selection by Recurrent Neural Networks Bartosz Piotrowski and Josef Urban In:LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving Agnieszka Słowik, Chaitanya Mangla, Mateja Jamnik, Sean Holden and Lawrence Paulson In:Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops
Towards Word Sense Disambiguation by Reasoning Javier Álvez, Itziar Gonzalez-Dios and German Rigau In:Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops
Using Vampire with Support for Algebraic Datatypes in Type Soundness Proofs Sylvia Grewe, André Pacak and Mira Mezini In:Vampire 2017. Proceedings of the 4th Vampire Workshop
An Inference Rule for the Acyclicity Property of Term Algebras Simon Robillard In:Vampire 2017. Proceedings of the 4th Vampire Workshop
We know (nearly) nothing!l But can we learn? Stephan Schulz In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Automated Invention of Strategies and Term Orderings for Vampire Jan Jakubuv, Martin Suda and Josef Urban In:GCAI 2017. 3rd Global Conference on Artificial Intelligence
Blocked Clauses in First-Order Logic Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits and Armin Biere In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Theorem Provers For Every Normal Modal Logic Tobias Gleißner, Alexander Steen and Christoph Benzmüller In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Better Proof Output for Vampire Giles Reger In:Vampire 2016. Proceedings of the 3rd Vampire Workshop
Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry Josef Urban and Robert Veroff In:IWIL-2015. 11th International Workshop on the Implementation of Logics
Implementing Polymorphism in Zenon Guillaume Bury, Raphaël Cauderlier and Pierre Halmagrand In:IWIL-2015. 11th International Workshop on the Implementation of Logics
SAT solving experiments in Vampire Armin Biere, Ioan Dragan, Laura Kovács and Andrei Voronkov In:Proceedings of the 1st and 2nd Vampire Workshops
Breeding Theorem Proving Heuristics with Genetic Algorithms Simon Schäfer and Stephan Schulz In:GCAI 2015. Global Conference on Artificial Intelligence
BliStr: The Blind Strategymaker Josef Urban In:GCAI 2015. Global Conference on Artificial Intelligence
Dialogues for proof search Jesse Alama In:ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics
A Logic for Verifying Metric Temporal Properties in Distributed Hybrid Systems Ping Hou and Yifei Chen In:ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics
Problem Libraries for Non-Classical Logics Jens Otten and Thomas Raths In:ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics
Beagle as a HOL4 external ATP method Thibault Gauthier, Cezary Kaliszyk, Chantal Keller and Michael Norrish In:PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning
Automated Theorem Proving using the TPTP Process Instruction Language Muhammad Nassar and Geoff Sutcliffe In:PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning
The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics Negin Arhami and Geoff Sutcliffe In:PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning
Understanding LEO-II’s proofs Nik Sultana and Christoph Benzmüller In:IWIL 2012. The 9th International Workshop on the Implementation of Logics
Efficient Rule-Matching for Hyper-Tableaux Bjarne Holen, Dag Hovland and Martin Giese In:IWIL 2012. The 9th International Workshop on the Implementation of Logics
Implementing Different Proof Calculi for First-order Modal Logics Christoph Benzmüller, Jens Otten and Thomas Raths In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
Learning from Multiple Proofs: First Experiments Daniel Kuehlwein and Josef Urban In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
Escape to Mizar from ATPs Jesse Alama In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
HipSpec : Automating Inductive Proofs of Program Properties Koen Claessen, Moa Johansson, Dan Rosen and Nick Smallbone In:ATx'12/WInG'12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation
User-friendly Support for Common Mathematical Concepts in a Lightweight Verifier Andrei Lapets In:VERIFY-2010. 6th International Verification Workshop
Tableau Calculus for Dummett Logic Based on Present and Next State of Knowledge Guido Fiorino In:IWIL 2010. The 8th International Workshop on the Implementation of Logics