Keyword:first-order logic

Papers
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 no. 9551
A Multithreaded Vampire with Shared Persistent Grounding Michael Rawson and Giles Reger EasyChair Preprint no. 5855
Making Theory Reasoning Simpler Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint no. 5000
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)
E 2.4 User Manual Stephan Schulz EasyChair Preprint no. 2272
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
The Aspect Calculus David Plaisted EasyChair Preprint no. 1256
Induction in Saturation-Based Proof Search Giles Reger and Andrei Voronkov EasyChair Preprint no. 826
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
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann EasyChair Preprint no. 396
Extending VIAP to Handle Array Programs Pritom Rajkhowa and Fangzhen Lin EasyChair Preprint no. 393
Partial Regularization of First-Order Resolution Proofs Jan Gorzny, Ezequiel Postan and Bruno Woltzenlogel Paleo EasyChair Preprint no. 360
Traversal-invariant definability and Logarithmic-space computation Steven Lindell and Scott Weinstein EasyChair Preprint no. 352
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
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
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
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
Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning Giles Reger, Martin Suda and Andrei Voronkov EasyChair Preprint no. 1
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
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
Global Subsumption Revisited (Briefly) Giles Reger and Martin Suda In:Vampire 2016. Proceedings of the 3rd Vampire Workshop
Better Proof Output for Vampire Giles Reger In:Vampire 2016. Proceedings of the 3rd Vampire Workshop
New Techniques in Clausal Form Generation Giles Reger, Martin Suda and Andrei Voronkov In:GCAI 2016. 2nd Global Conference on Artificial Intelligence
AVATAR Modulo Theories Giles Reger, Nikolaj Bjorner, 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