| Publication | Date of Publication | Type |
|---|
Mizar 60 for Mizar 50
| 2024-11-26 | Paper |
Vampire getting noisy: Will random bits help conquer chaos? (system description)
| 2022-12-07 | Paper |
Layered clause selection for theory reasoning (short paper)
| 2022-11-09 | Paper |
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
Automated Reasoning | 2022-11-09 | Paper |
Testing a saturation-based theorem prover: experiences and challenges
Tests and Proofs | 2022-07-01 | Paper |
Vampire with a brain is a good ITP hammer
| 2022-03-24 | Paper |
SAT competition 2020
Artificial Intelligence | 2021-12-13 | Paper |
Improving ENIGMA-style clause selection while learning from history
| 2021-12-01 | Paper |
Neural precedence recommender
| 2021-12-01 | Paper |
Introduction: Fundamental principles of quantum random number generation with beam splitters
Quantum Science and Technology | 2020-07-01 | Paper |
Quantum Random Number Generation
Quantum Science and Technology | 2020-07-01 | Paper |
Symmetry avoidance in MACE-style finite model finding
| 2020-05-13 | Paper |
ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
| 2020-03-10 | Paper |
Unification with abstraction and theory instantiation in saturation-based reasoning
| 2019-09-16 | Paper |
Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
Journal of Automated Reasoning | 2019-09-02 | Paper |
A theory of satisfiability-preserving proofs in SAT solving
EPiC Series in Computing | 2019-07-04 | Paper |
Towards Smarter MACE-style Model Finders
EPiC Series in Computing | 2019-07-04 | Paper |
Blocked clauses in first-order logic
EPiC Series in Computing | 2019-01-10 | Paper |
Local soundness for QBF calculi
| 2018-08-10 | Paper |
A unifying principle for clause elimination in first-order logic
| 2017-09-22 | Paper |
Splitting proofs for interpolation
| 2017-09-22 | Paper |
Selecting the selection
Automated Reasoning | 2016-09-05 | Paper |
Lifting QBF resolution calculi to DQBF
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Finding Finite Models in Multi-sorted First-Order Logic
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
Playing with AVATAR
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
Variable and clause elimination for LTL satisfiability checking
Mathematics in Computer Science | 2015-10-30 | Paper |
Property directed reachability for automated planning
Journal of Artificial Intelligence Research | 2014-06-23 | Paper |
A PLTL-prover based on labelled superposition with partial model guidance
Automated Reasoning | 2012-09-05 | Paper |
Labelled superposition for PLTL
Logic for Programming, Artificial Intelligence, and Reasoning | 2012-06-15 | Paper |
On the saturation of YAGO
Automated Reasoning | 2010-09-14 | Paper |
A NOVEL ATTACK STRATEGY ON ENTANGLEMENT SWAPPING QKD PROTOCOLS
International Journal of Quantum Information | 2008-11-17 | Paper |
