| Entailment is Undecidable for Symbolic Heap Separation Logic Formulæ with Non-Established Inductive Rules | 0 | 0.34 | 2022 |
| Decidable Entailments in Separation Logic with Inductive Definitions - Beyond Establishment. | 0 | 0.34 | 2021 |
| Unifying Decidable Entailments In Separation Logic With Inductive Definitions | 0 | 0.34 | 2021 |
| A Superposition-Based Calculus for Diagrammatic Reasoning. | 0 | 0.34 | 2021 |
| The Bernays-Schönfinkel-Ramsey Class of Separation Logic with Uninterpreted Predicates | 0 | 0.34 | 2020 |
| Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard | 0 | 0.34 | 2020 |
| The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains. | 0 | 0.34 | 2019 |
| On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic. | 0 | 0.34 | 2018 |
| The Complexity of Prenex Separation Logic with One Selector. | 0 | 0.34 | 2018 |
| A Generic Framework for Implicate Generation Modulo Theories. | 0 | 0.34 | 2018 |
| Prime Implicate Generation in Equational Logic (extended abstract). | 0 | 0.34 | 2018 |
| Pricing in discrete financial models. | 0 | 0.34 | 2018 |
| Formalizing the Cox–Ross–Rubinstein Pricing of European Derivatives in Isabelle/HOL | 0 | 0.34 | 2018 |
| The Binomial Pricing Model in Finance: A Formalization in Isabelle. | 1 | 0.37 | 2017 |
| Prime Implicate Generation in Equational Logic. | 1 | 0.36 | 2017 |
| Quantifier-Free Equational Logic and Prime Implicate Generation | 2 | 0.37 | 2015 |
| A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. | 0 | 0.34 | 2014 |
| A Rewriting Strategy to Generate Prime Implicates in Equational Logic. | 3 | 0.40 | 2014 |
| A Resolution Calculus for First-order Schemata | 7 | 0.56 | 2013 |
| Reasoning on schemata of formulæ | 0 | 0.34 | 2012 |
| A calculus for generating ground explanations | 4 | 0.42 | 2012 |
| A Calculus for Generating Ground Explanations (Technical Report) | 1 | 0.36 | 2012 |
| An Instantiation Scheme for Satisfiability Modulo Theories | 4 | 0.38 | 2012 |
| Instantiation Schemes for Nested Theories | 0 | 0.34 | 2011 |
| Solving Linear Constraints in Elementary Abelian p-Groups of Symmetries | 0 | 0.34 | 2011 |
| Modular instantiation schemes | 1 | 0.35 | 2011 |
| Instantiation of SMT problems modulo integers | 2 | 0.36 | 2010 |
| Theory decision by decomposition | 17 | 0.67 | 2010 |
| On Variable-inactivity and Polynomial T-Satisfiability Procedures | 18 | 0.66 | 2008 |
| Unification and Matching Modulo Leaf-Permutative Equational Presentations | 0 | 0.34 | 2008 |
| Permutative rewriting and unification | 3 | 0.40 | 2007 |
| Determining Unify-Stable Presentations | 1 | 0.36 | 2007 |
| Rewrite-Based Satisfiability Procedures for Recursive Data Structures | 6 | 0.49 | 2007 |
| T-Decision by Decomposition | 3 | 0.39 | 2007 |
| Rewrite-Based Decision Procedures | 6 | 0.44 | 2007 |
| Unification in a class of permutative theories | 1 | 0.36 | 2005 |
| Overlapping Leaf Permutative Equations | 4 | 0.48 | 2004 |
| On the Complexity of Deduction Modulo Leaf Permutative Equations | 3 | 0.47 | 2004 |
| On leaf permutative theories and occurrence permutation groups | 3 | 0.51 | 2003 |
| NP-Completeness Results for Deductive Problems on Stratified Terms | 4 | 0.51 | 2003 |
