Keyword:automated reasoning

Publications
Divide and Conquer: a Compositional Approach to Game-Theoretic Security Ivana Bocevska, Anja Petković Komel, Laura Kovács, Sophie Rain and Michael Rawson EasyChair Preprint 15785
Towards Computer-Assisted Proofs of Parametric Andrews-Curtis Simplifications, II Alexei Lisitsa EasyChair Preprint 13320
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic (Extended Version) Johannes Schoisswohl, Laura Kovács and Konstantin Korovin EasyChair Preprint 13150
CheckMate: Automated Game-Theoretic Security Reasoning Lea Salome Brugger, Laura Kovács, Anja Petković Komel, Sophie Rain and Michael Rawson EasyChair Preprint 10853
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovacs, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 9606
Induction with Recursive Definitions in Superposition Marton Hajdu, Petra Hozzová, Laura Kovacs and Andrei Voronkov EasyChair Preprint 6513
Inductive Benchmarks for Automated Reasoning Márton Hajdu, Petra Hozzová, Laura Kovács, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 5531
Integer Induction in Saturation Petra Hozzová, Laura Kovács and Andrei Voronkov EasyChair Preprint 5176
Making Theory Reasoning Simpler Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 5000
Distributed Automated Fuzzy Reasoning Systems Venkata Subba Reddy Poli EasyChair Preprint 3260
Induction with Generalization in Superposition Reasoning Márton Hajdu, Petra Hozzová, Laura Kovács, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint 2468
E 2.4 User Manual Stephan Schulz EasyChair Preprint 2272
Directed Graph Networks for Logical Entailment Michael Rawson and Giles Reger EasyChair Preprint 2185
Induction in Saturation-Based Proof Search Giles Reger and Andrei Voronkov EasyChair Preprint 826
Åqvist's Dyadic Deontic Logic E in HOL Christoph Benzmüller, Ali Farjami and Xavier Parent EasyChair Preprint 554
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
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
Scaling CheckMate for Game-Theoretic Security Sophie Rain, Lea Salome Brugger, Anja Petković Komel, Laura Kovács and Michael Rawson In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Saturating Sorting without Sorts Pamina Georgiou, Marton Hajdu and Laura Kovács In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Towards computer-assisted proofs of parametric Andrews-Curtis simplifications, II Alexei Lisitsa In:LPAR 2024 Complementary Volume
Automated Reasoning with Tangles: towards Quantum Verification Applications Andrew Fish and Alexei Lisitsa In:LPAR 2024 Complementary Volume
The Spawns of the Saturation Framework Sophie Tourret In:Proceedings of the 7th and 8th Vampire Workshop
Embedding Intuitionistic into Classical Logic Alexander Pluska and Florian Zuleger In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
On the Complexity of Convex and Reverse Convex Prequadratic Constraints Rodrigo Raya, Jad Hamza and Viktor Kuncak In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Decision levels are stable: towards better SAT heuristics Robert Nieuwenhuis, Adrià Lozano, Albert Oliveras and Enric Rodríguez-Carbonell In:LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Learning Ex Nihilo Selmer Bringsjord, Naveen Sundar Govindarajulu, John Licato and Michael Giancola In:GCAI 2020. 6th Global Conference on Artificial Intelligence (GCAI 2020)
Experimenting with Theory Instantiation in Vampire Martin Riener In:Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops
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
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
SC-square: when Satisfiability Checking and Symbolic Computation join forces Erika Abraham, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening and Werner M. Seiler In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
AI at CADE/IJCAR Josef Urban In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Reasoning Inside The Box: Deduction in Herbrand Logics Liron Cohen and Yoni Zohar In:GCAI 2017. 3rd Global Conference on Artificial Intelligence
TacticToe: Learning to Reason with HOL4 Tactics Thibault Gauthier, Cezary Kaliszyk and Josef Urban 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
RACCOON: A Connection Reasoner for the Description Logic ALC Dimas Melo Filho, Fred Freitas and Jens Otten In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
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
Improving Statistical Linguistic Algorithms for Parsing Mathematics Cezary Kaliszyk, Josef Urban and Jiri Vyskocil In:IWIL-2015. 11th International Workshop on the Implementation of Logics
Determining automatically compass and straightedge unconstructibility in triangles Pascal Mathis and Pascal Schreck In:SCSS 2016. 7th International Symposium on Symbolic Computation in Software Science
Reasoning About Loops Using Vampire Laura Kovács and Simon Robillard In:Proceedings of the 1st and 2nd Vampire Workshops
Machine Learner for Automated Reasoning 0.4 and 0.5 Cezary Kaliszyk, Josef Urban and Jiri Vyskocil In:PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning
Building an Efficient OWL 2 DL Reasoner Boris Motik In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
Practical Aspects of SAT Solving Armin Biere In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora Cezary Kaliszyk and Josef Urban 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
Experiments on the feasibility of using a floating-point simplex in an SMT solver Diego Caminha Barbosa de Oliveira and David Monniaux In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
BDD-based automated reasoning in propositional non-classical logics: progress report Rajeev Gore and Jimmy Thomson In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
Escape to Mizar from ATPs Jesse Alama In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
CDCL with Less Destructive Backtracking through Partial Ordering Anthony Monnet and Roger Villemaire In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
Synthesising Functional Invariants in Separation Logic Ewen Maclean, Andrew Ireland and Gudmund Grov In:WING 2010. Workshop on Invariant Generation 2010
Automated Reasoning in the Simulation of Evolvable Systems Djihed Afifi, David Rydeheard and Howard Barringer In:PAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning
Automated Higher-order Reasoning about Quantales Han-Hing Dang and Peter Höfner In:PAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning