Keyword:theorem proving

Publications
Synthesis of Recursive Programs in Saturation Petra Hozzová, Daneshvar Amrollahi, Márton Hajdu, Laura Kovács, Andrei Voronkov and Eva Maria Wagner EasyChair Preprint 12145
Program Synthesis in Saturation Petra Hozzová, Laura Kovács, Chase Norman and Andrei Voronkov EasyChair Preprint 10223
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovacs, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 9606
Formalization of Transform Methods in Higher-Order Logic: a Survey Muhammad Ahmed and Adnan Rashid EasyChair Preprint 8009
Formalization of Gambler’s Ruin Problem in Isabelle/HOL Zibo Yang EasyChair Preprint 6165
Formalization of RBD-based Cause Consequence Analysis in HOL Mohamed Abdelghany and Sofiene Tahar EasyChair Preprint 5720
Integer Induction in Saturation Petra Hozzová, Laura Kovács and Andrei Voronkov EasyChair Preprint 5176
Context-aware Generation of Proof Scripts for Theorem Proving Cheng Chuanhu, Yan Xiong, Wenchao Huang and Ma Lu EasyChair Preprint 3341
Automated Theorem Proving in a Chat Environment Rustam Zhumagambetov and Mark Sterling EasyChair Preprint 447
Certified Graph View Maintenance with Regular Datalog Angela Bonifati, Stefania Dumbrava and Emilio Jesús Gallego Arias EasyChair Preprint 211
Automated Theorem Proving by Translation to Description Logic Negin Arhami and Geoff Sutcliffe EasyChair Preprint 126
Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning Giles Reger, Martin Suda and Andrei Voronkov EasyChair Preprint 1
First Experiments with Neural cvc5 Jelle Piepenbrock, Mikolas Janota, Josef Urban and Jan Jakubův In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
ARCH-COMP23 Category Report: Hybrid Systems Theorem Proving Stefan Mitsch, Huanhuan Sheng, Bohua Zhan, Shuling Wang, Simon Foster and Jonathan Julian Huerta Y Munive In:Proceedings of 10th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH23)
Guiding an Instantiation Prover with Graph Neural Networks Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock and Josef Urban In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Keep me out of the loop: a more flexible choreographic projection Luís Cruz-Filipe, Fabrizio Montesi and Robert R. Rasmussen In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
ARCH-COMP22 Category Report: Hybrid Systems Theorem Proving Stefan Mitsch, Bohua Zhan, Huanhuan Sheng, Alexander Bentkamp, Xiangyu Jin, Shuling Wang, Simon Foster, Christian Pardillo Laursen and Jonathan Julián Huerta Y Munive In:Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22)
ARCH-COMP21 Category Report: Hybrid Systems Theorem Proving Stefan Mitsch, Xiangyu Jin, Bohua Zhan, Shuling Wang and Naijun Zhan In:8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21)
ARCH-COMP20 Category Report:Hybrid Systems Theorem Proving Stefan Mitsch, Jonathan Julián Huerta Y Munive, Xiangyu Jin, Bohua Zhan, Shuling Wang and Naijun Zhan In:ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20)
CoRg: Commonsense Reasoning Using a Theorem Prover and Machine Learning Sophie Siebert and Frieder Stolzenburg In:Selected Student Contributions and Workshop Papers of LuxLogAI 2018
Revisiting Question Answering in Vampire Giles Reger In:Vampire 2017. Proceedings of the 4th Vampire Workshop
Incremental Solving with Vampire Giles Reger and Martin Suda In:Vampire 2017. Proceedings of the 4th Vampire Workshop
On Conflict-Driven Reasoning Maria Paola Bonacina In:Automated Formal Methods
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
Reasoning about Translation Lookaside Buffers Hira Syeda and Gerwin Klein 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
Global Subsumption Revisited (Briefly) Giles Reger and Martin Suda In:Vampire 2016. Proceedings of the 3rd Vampire Workshop
A Clausal Normal Form Translation for FOOL Evgenii Kotelnikov, Laura Kovács, 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
New Techniques in Clausal Form Generation Giles Reger, Martin Suda and Andrei Voronkov In:GCAI 2016. 2nd Global Conference on Artificial Intelligence
The Uses of SAT Solvers in Vampire Giles Reger and Martin Suda In:Proceedings of the 1st and 2nd Vampire Workshops
Things You Can't do With a Vampire Geoff Sutcliffe In:Proceedings of the 1st and 2nd Vampire Workshops
Automated Theorem Proving by Translation to Description Logic Negin Arhami and Geoff Sutcliffe In:LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations
Proof Support for Common Logic Till Mossakowski, Mihai Codescu, Oliver Kutz, Christoph Lange and Michael Grüninger In:ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics
Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic Hans De Nivelle In:ARQNL 2014. Automated Reasoning in Quantified Non-Classical Logics
Polymorphic+Typeclass Superposition Daniel Wand In:PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning
Instantiations, Zippers and EPR Interpolation Nikolaj Bjorner, Arie Gurfinkel, Konstantin Korovin and Ori Lahav In:LPAR-19. 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
A Framework for Verified Depth-First Algorithms René Neumann In:ATx'12/WInG'12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation
Logical and Algebraic Views of a Knot Fold of a Regular Heptagon Fadoua Ghourabi, Tetsuo Ida and Kazuko Takahashi In:SCSS 2013. 5th International Symposium on Symbolic Computation in Software Science
Formal Requirements Capturing using VRS system Alexander Letichevsky, Alexander Kolchin, Oleksandr Letychevskyy jr., Stepan Potiyenko, Vlad Volkov and Thomas Weigert In:WING 2010. Workshop on Invariant Generation 2010
Cocktail II Michael Franssen In:WING 2010. Workshop on Invariant Generation 2010
Extending Non-Termination Proof Techniques to Asynchronously Communicating Concurrent Programs Matthias Kuntz, Stefan Leue and Christoph Scheben In:WING 2010. Workshop on Invariant Generation 2010