| Combining Constraint Solving and Bayesian Techniques for System Optimization. | 0 | 0.34 | 2022 |
| The Ksmt Calculus Is A Delta-Complete Decision Procedure For Non-Linear Constraints | 0 | 0.34 | 2021 |
| Implementing Superposition in iProver (System Description). | 0 | 0.34 | 2020 |
| Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation | 0 | 0.34 | 2020 |
| An Abstraction-Refinement Framework for Reasoning with Large Theories | 0 | 0.34 | 2018 |
| Premise selection with neural networks and distributed representation of features. | 0 | 0.34 | 2018 |
| Computing exponentially faster: Implementing a nondeterministic universal Turing machine using DNA. | 1 | 0.38 | 2016 |
| Predicate Elimination for Preprocessing in First-Order Theorem Proving. | 2 | 0.38 | 2016 |
| EPR-based k-induction with Counterexample Guided Abstraction Refinement. | 0 | 0.34 | 2015 |
| Non-cyclic Sorts for First-Order Satisfiability. | 4 | 0.41 | 2013 |
| Inst-Gen - A Modular Approach to Instantiation-Based Automated Reasoning. | 18 | 0.85 | 2013 |
| From Resolution and DPLL to Solving Arithmetic Constraints. | 1 | 0.35 | 2013 |
| Bound Propagation for Arithmetic Reasoning in Vampire | 1 | 0.37 | 2013 |
| EPR-based bounded model checking at word level | 3 | 0.44 | 2012 |
| Preprocessing techniques for first-order clausification. | 4 | 0.41 | 2012 |
| GoRRiLA and hard reality | 3 | 0.43 | 2011 |
| Implementing conflict resolution | 1 | 0.37 | 2011 |
| Solving systems of linear inequalities by bound propagation | 9 | 0.92 | 2011 |
| iProver-Eq: an instantiation-based theorem prover with equality | 10 | 0.47 | 2010 |
| Labelled unit superposition calculi for instantiation-based reasoning | 2 | 0.37 | 2010 |
| Encoding industrial hardware verification problems into effectively propositional logic | 7 | 0.47 | 2010 |
| Instantiation-Based Automated Reasoning: From Theory to Practice | 12 | 0.73 | 2009 |
| iProver --- An Instantiation-Based Theorem Prover for First-Order Logic (System Description) | 58 | 1.96 | 2008 |
| Integrating linear arithmetic into superposition calculus | 33 | 1.54 | 2007 |
| Random databases and threshold for monotone non-recursive datalog | 0 | 0.34 | 2005 |
| Knuth-Bendix Constraint Solving Is NP-Complete | 12 | 1.11 | 2005 |
| Orienting rewrite rules with the Knuth--Bendix order | 25 | 1.11 | 2003 |
| Orienting equalities with the Knuth-Bendix order | 2 | 0.40 | 2003 |
| New directions in instantiation-based theorem proving | 50 | 1.81 | 2003 |
| An AC-Compatible Knuth-Bendix Order | 3 | 0.37 | 2003 |
| The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures | 2 | 0.38 | 2002 |
| Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order | 9 | 0.96 | 2001 |
| A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering | 16 | 0.93 | 2000 |
