| Publication | Date of Publication | Type |
|---|
Invariant neural architecture for learning term synthesis in instantiation proving
Journal of Symbolic Computation | 2024-12-09 | Paper |
Graph sequence learning for premise selection
Journal of Symbolic Computation | 2024-12-09 | Paper |
| ALASCA: reasoning in quantified linear arithmetic | 2023-12-13 | Paper |
The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints
Theoretical Computer Science | 2023-09-21 | Paper |
| Ground joinability and connectedness in the superposition calculus | 2022-12-07 | Paper |
Implementing Superposition in iProver (System Description)
Automated Reasoning | 2022-11-09 | Paper |
AC simplifications and closure redundancies in the superposition calculus
(available as arXiv preprint) | 2022-05-25 | Paper |
| Heterogeneous heuristic optimisation and scheduling for first-order theorem proving | 2022-04-22 | Paper |
The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
(available as arXiv preprint) | 2021-12-01 | Paper |
A CDCL-style calculus for solving non-linear constraints
(available as arXiv preprint) | 2020-05-13 | Paper |
| An abstraction-refinement framework for reasoning with large theories | 2018-10-18 | Paper |
Knuth--bendix constraint solving is NP-complete
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Predicate Elimination for Preprocessing in First-Order Theorem Proving
Theory and Applications of Satisfiability Testing – SAT 2016 | 2016-09-05 | Paper |
GoRRiLA and Hard Reality
Perspectives of Systems Informatics | 2015-12-07 | Paper |
Implementing conflict resolution
Perspectives of Systems Informatics | 2015-12-07 | Paper |
Towards conflict-driven learning for virtual substitution
Computer Algebra in Scientific Computing | 2014-09-08 | Paper |
Skolemization modulo theories
Mathematical Software – ICMS 2014 | 2014-09-08 | Paper |
Non-cyclic sorts for first-order satisfiability
Frontiers of Combining Systems | 2013-09-20 | Paper |
Inst-Gen -- a modular approach to instantiation-based automated reasoning
Programming Logics | 2013-04-19 | Paper |
EPR-based bounded model checking at word level
Automated Reasoning | 2012-09-05 | Paper |
Solving systems of linear inequalities by bound propagation
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Labelled unit superposition calculi for instantiation-based reasoning
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
iProver-Eq: An Instantiation-Based Theorem Prover with Equality
Automated Reasoning | 2010-09-14 | Paper |
An AC-compatible Knuth-Bendix order.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Conflict Resolution
Principles and Practice of Constraint Programming - CP 2009 | 2009-10-09 | Paper |
Integrating Linear Arithmetic into Superposition Calculus
Computer Science Logic | 2009-03-05 | Paper |
iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
Automated Reasoning | 2008-11-27 | Paper |
Theory Instantiation
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Mathematical Foundations of Computer Science 2005
Lecture Notes in Computer Science | 2006-10-20 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2005-08-22 | Paper |
Orienting rewrite rules with the Knuth-Bendix order.
Information and Computation | 2003-08-19 | Paper |
| scientific article; zbMATH DE number 1954387 (Why is no real title available?) | 2003-07-28 | Paper |
| scientific article; zbMATH DE number 1754649 (Why is no real title available?) | 2002-06-12 | Paper |
| scientific article; zbMATH DE number 1722704 (Why is no real title available?) | 2002-03-21 | Paper |
