Keyword:automated theorem proving

Papers
Lazy and Eager Patterns in High-Performance Automated Theorem Proving Stephan Schulz In:Proceedings of the 7th and 8th Vampire Workshop
Sorting Without Sorts Pamina Georgiou, Márton Hajdu and Laura Kovács EasyChair Preprint no. 10632
Lazy and Eager Patterns in High-Performance Automated Theorem Proving Stephan Schulz EasyChair Preprint no. 10510
Refining Unification with Abstraction Ahmed Bhayat, Konstantin Korovin, Laura Kovács 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
Model Based Interpolation for Uninterpreted Functions and Integer Linear Arithmetic Nikolaj Bjorner, Arie Gurfinkel, Sharon Shoham and Yakir Vizel EasyChair Preprint no. 10000
Goéland: a Concurrent Tableau-Based Theorem Prover (System Description) Julie Cailler, Johann Rosain, David Delahaye, Simon Robillard and Hinde Bouziane EasyChair Preprint no. 8676
A Multithreaded Vampire with Shared Persistent Grounding Michael Rawson and Giles Reger EasyChair Preprint no. 5855
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 C. 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
E 2.4 User Manual Stephan Schulz EasyChair Preprint no. 2272
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
A FOOLish Encoding of the Next State Relations of Imperative Programs Evgenii Kotelnikov, Laura Kovács and Andrei Voronkov EasyChair Preprint no. 98
E 2.0 User Manual Stephan Schulz EasyChair Preprint no. 8
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
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
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
Better Proof Output for Vampire Giles Reger In:Vampire 2016. Proceedings of the 3rd Vampire Workshop
Implementing Polymorphism in Zenon Guillaume Bury, Raphaël Cauderlier and Pierre Halmagrand In:IWIL-2015. 11th International Workshop on the Implementation of Logics
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
SAT solving experiments in Vampire Armin Biere, Ioan Dragan, Laura Kovács and Andrei Voronkov In:Proceedings of the 1st and 2nd Vampire Workshops
BliStr: The Blind Strategymaker Josef Urban In:GCAI 2015. Global Conference on Artificial Intelligence
Breeding Theorem Proving Heuristics with Genetic Algorithms Simon Schäfer and Stephan Schulz In:GCAI 2015. Global Conference on Artificial Intelligence
Problem Libraries for Non-Classical Logics Jens Otten and Thomas Raths 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
Dialogues for proof search Jesse Alama In:ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics
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
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
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
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
Understanding LEO-II’s proofs Nik Sultana and Christoph Benzmüller In:IWIL 2012. The 9th International Workshop on the Implementation of Logics
Escape to Mizar from ATPs Jesse Alama 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
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
HipSpec : Automating Inductive Proofs of Program Properties Koen Claessen, Moa Johansson, Dan Rosén and Nicholas 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