Keyword:first-order logic

Publications
Gödel Mathematics Versus Hilbert Mathematics. II Logicism and Hilbert Mathematics, the Identification of Logic and Set Theory, and Gödel’s “Completeness Paper” (1930) Vasil Penchev EasyChair Preprint 9551
A Multithreaded Vampire with Shared Persistent Grounding Michael Rawson and Giles Reger EasyChair Preprint 5855
Making Theory Reasoning Simpler Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 5000
E 2.4 User Manual Stephan Schulz EasyChair Preprint 2272
The Aspect Calculus David Plaisted EasyChair Preprint 1256
Induction in Saturation-Based Proof Search Giles Reger and Andrei Voronkov EasyChair Preprint 826
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann EasyChair Preprint 396
Extending VIAP to Handle Array Programs Pritom Rajkhowa and Fangzhen Lin EasyChair Preprint 393
Partial Regularization of First-Order Resolution Proofs Jan Gorzny, Ezequiel Postan and Bruno Woltzenlogel Paleo EasyChair Preprint 360
Traversal-invariant definability and Logarithmic-space computation Steven Lindell and Scott Weinstein EasyChair Preprint 352
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
Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning Giles Reger, Martin Suda and Andrei Voronkov EasyChair Preprint 1
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
Property Preserving Embedding of First-order Logic Julian Parsert, Stephanie Autherith and Cezary Kaliszyk In:GCAI 2020. 6th Global Conference on Artificial Intelligence (GCAI 2020)
Partial Regularization of First-Order Resolution Proofs Jan Gorzny, Ezequiel Postan and Bruno Woltzenlogel Paleo In:GCAI 2020. 6th Global Conference on Artificial Intelligence (GCAI 2020)
DLS-Forgetter: An Implementation of the DLS Forgetting Calculus for First-Order Logic Ruba Alassaf and Renate A. Schmidt In:GCAI 2019. Proceedings of the 5th Global Conference on Artificial Intelligence
Loop Analysis by Quantification over Iterations Bernhard Gleiss, Laura Kovács and Simon Robillard In:LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Checkable Proofs for First-Order Theorem Proving Giles Reger and Martin Suda In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
The Potential of Interference-Based Proof Systems Marijn Heule and Benjamin Kiesl 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
Deep Network Guided Proof Search Sarah Loos, Geoffrey Irving, Christian Szegedy and Cezary Kaliszyk 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
Global Subsumption Revisited (Briefly) Giles Reger and Martin Suda In:Vampire 2016. Proceedings of the 3rd Vampire Workshop
AVATAR Modulo Theories Giles Reger, Nikolaj Bjorner, Martin Suda and Andrei Voronkov In:GCAI 2016. 2nd Global Conference on Artificial Intelligence
New Techniques in Clausal Form Generation Giles Reger, Martin Suda and Andrei Voronkov In:GCAI 2016. 2nd Global Conference on Artificial Intelligence
Implementing Polymorphism in Zenon Guillaume Bury, Raphaël Cauderlier and Pierre Halmagrand In:IWIL-2015. 11th International Workshop on the Implementation of Logics
EPR-based k-induction with Counterexample Guided Abstraction Refinement Zurab Khasidashvili, Konstantin Korovin and Dmitry Tsarkov In:GCAI 2015. Global Conference on Artificial Intelligence
A Lightweight Double-negation Translation Frederic Gilbert In:LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations
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
Scheme representation for first-order logic Steve Awodey and Spencer Breiner In:TACL 2013. Sixth International Conference on Topology, Algebra and Categories in Logic
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