Keyword:theorem proving

Papers
Program Synthesis in Saturation Petra Hozzová, Laura Kovács, Chase Norman and Andrei Voronkov EasyChair Preprint no. 10223
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint no. 9606
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)
Formalization of Transform Methods in Higher-Order Logic: a Survey Muhammad Ahmed and Adnan Rashid EasyChair Preprint no. 8009
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)
Formalization of Gambler’s Ruin Problem in Isabelle/HOL Zibo Yang EasyChair Preprint no. 6165
Formalization of RBD-based Cause Consequence Analysis in HOL Mohamed Abdelghany and Sofiene Tahar EasyChair Preprint no. 5720
Integer Induction in Saturation Petra Hozzová, Laura Kovács and Andrei Voronkov EasyChair Preprint no. 5176
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)
Context-aware Generation of Proof Scripts for Theorem Proving Cheng Chuanhu, Yan Xiong, Wenchao Huang and Ma Lu EasyChair Preprint no. 3341
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
Automated Theorem Proving in a Chat Environment Rustam Zhumagambetov and Mark Sterling EasyChair Preprint no. 447
Incremental Solving with Vampire Giles Reger and Martin Suda In:Vampire 2017. Proceedings of the 4th Vampire Workshop
Revisiting Question Answering in Vampire Giles Reger In:Vampire 2017. Proceedings of the 4th Vampire Workshop
Certified Graph View Maintenance with Regular Datalog Angela Bonifati, Stefania Dumbrava and Emilio Jesús Gallego Arias EasyChair Preprint no. 211
Automated Theorem Proving by Translation to Description Logic Negin Arhami and Geoff Sutcliffe EasyChair Preprint no. 126
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
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
Reasoning about Translation Lookaside Buffers Hira Syeda and Gerwin Klein 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
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
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
Things You Can't do With a Vampire Geoff Sutcliffe In:Proceedings of the 1st and 2nd Vampire Workshops
The Uses of SAT Solvers in Vampire Giles Reger and Martin Suda 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
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
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
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
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
Cocktail II Michael Franssen In:WING 2010. Workshop on Invariant Generation 2010
Formal Requirements Capturing using VRS system Alexander Letichevsky, Alexander Kolchin, Oleksandr Letychevskyi, Stepan Potiyenko, Vlad Volkov and Thomas Weigert In:WING 2010. Workshop on Invariant Generation 2010