Publications

2024

  1. Article
    RG1
    “Reduction of Chemical Reaction Networks with Approximate Conservation Laws,” SIAM journal on Applied Dynamical Systems, vol. 23, no. 1, 2024.

2023

  1. Article
    RG1
    “Mechanical Mathematicians,” Communications of the ACM, vol. 66, no. 4, 2023.
  2. Article
    RG1
    “Superposition for Higher-Order Logic,” Journal of Automated Reasoning, vol. 67, no. 1, 2023.
  3. Article
    RG1
    “Given Clause Loops,” Archive of Formal Proofs, 2023.
  4. Conference paper
    RG1
    “Verified Given Clause Procedures,” in Automated Deductions -- CADE 29, Rome, Italy, 2023.
  5. Conference paper
    RG1
    “KBO Constraint Solving Revisited,” in Frontiers of Combining Systems (FroCoS 2023), Prague, Czech Republic, 2023.
  6. Conference paper
    RG1
    “An Isabelle/HOL Formalization of the SCL(FOL) Calculus,” in Automated Deductions -- CADE 29, Rome, Italy, 2023.
  7. Conference paper
    RG1
    “SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning,” in Automated Deductions -- CADE 29, Rome, Italy, 2023.
  8. Conference paper
    RG1
    “Symbolic Model Construction for Saturated Constrained Horn Clauses,” in Frontiers of Combining Systems (FroCoS 2023), Prague, Czech Republic, 2023.
  9. Paper
    RG1
    “SCL(FOL) Revisited,” 2023. [Online]. Available: https://arxiv.org/abs/2302.05954.
  10. Paper
    RG1
    “Explicit Model Construction for Saturated Constrained Horn Clauses,” 2023. [Online]. Available: https://arxiv.org/abs/2305.05064.
  11. Article
    RG1
    “Unifying Splitting,” Journal of Automated Reasoning, vol. 67, no. 2, 2023.
  12. Conference paper
    RG1
    “A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper),” in Automated Deductions -- CADE 29, Rome, Italy, 2023.
  13. Thesis
    RG1
    “On a Notion of Abduction and Relevance for First-Order Logic Clause Sets,” Universität des Saarlandes, Saarbrücken, 2023.
  14. Article
    RG1
    “Termination of Triangular Polynomial Loops,” Formal Methods in System Design, 2023.
  15. Article
    RG1
    “SCL(EQ): SCL for First-Order Logic with Equality,” Journal of Automated Reasoning, vol. 67, 2023.
  16. Conference paper
    RG1
    “An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL,” in Frontiers of Combining Systems (FroCoS 2023), Prague, Czech Republic, 2023.
  17. Article
    RG1
    “The 11th IJCAR automated theorem proving system competition – CASC-J11,” AI Communications, vol. 36, no. 2, 2023.

2022

  1. Article
    RG1
    “On the Algebraic Structures in A(Phi) (G),” Mediterranian Journal of Mathematics, vol. 19, no. 3, 2022.
  2. Paper
    RG1
    “SAT-Inspired Higher-Order Eliminations,” 2022. [Online]. Available: https://arxiv.org/abs/2208.07775.
  3. Conference paper
    RG1
    “A Two-Watched Literal Scheme for First-Order Logic,” in Practical Aspects of Automated Reasoning 2022 (PAAR 2022), Haifa, Israel, 2022.
  4. Conference paper
    RG1
    “An Efficient Subsumption Test Pipeline for BS(LRA) Clauses,” in Automated Reasoning (IJCAR 2022), Haifa, Israel, 2022.
  5. Conference paper
    RG1
    “Exploring Partial Models with SCL,” in Practical Aspects of Automated Reasoning 2022 (PAAR 2022), Haifa, Israel, 2022.
  6. Paper
    RG1
    “A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic,” 2022. [Online]. Available: https://arxiv.org/abs/2201.09769.
  7. Conference paper
    RG1
    “A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), Munich, Germany, 2022.
  8. Conference paper
    RG1
    “F5: A REDUCE Package for Signature-based Gröbner Basis Computation,” in CASC 2022 - Computer Algebra in Scientific Computing, Gebze, Turkey, 2022.
  9. Conference paper
    RG1
    “Seventeen Provers Under the Hammer,” in 13th International Conference on Interactive Theorem Proving (ITP 2022), Haifa, Israel, 2022.
  10. Article
    RG1
    “A Calculus for Modular Loop Acceleration and Non-Termination Proofs,” International Journal on Software Tools for Technology Transfer, vol. 24, 2022.
  11. Conference paper
    RG1
    “Connection-Minimal Abduction in EL via Translation to FOL (Extended Abstract),” in Description Logics 2022 (DL 2022), Haifa, Israel, 2022.
  12. Conference paper
    RG1
    “Connection-Minimal Abduction in EL via Translation to FOL,” in Automated Reasoning (IJCAR 2022), Haifa, Israel, 2022.
  13. Conference paper
    RG1
    “Semantic Relevance,” in Automated Reasoning (IJCAR 2022), Haifa, Israel, 2022.
  14. Paper
    RG1
    “Connection-minimal Abduction in EL via Translation to FOL -- Technical Report,” 2022. [Online]. Available: https://arxiv.org/abs/2205.08449.
  15. Conference paper
    RG1
    “SCL(EQ): SCL for First-Order Logic with Equality,” in Automated Reasoning (IJCAR 2022), Haifa, Israel, 2022.
  16. Paper
    RG1
    “SCL(EQ): SCL for First-Order Logic with Equality,” 2022. [Online]. Available: https://arxiv.org/abs/2205.08297.
  17. Conference paper
    RG1
    “Automated Expected Amortised Cost Analysis of Probabilistic Data Structures,” in Computer Aided Verification (CAV 2022), Haifa, Israel, 2022.
  18. Paper
    RG1
    “ODEbase: A Repository of ODE Systems for Systems Biology,” 2022. [Online]. Available: https://arxiv.org/abs/2201.08980.
  19. Article
    RG1
    “ODEbase: A Repository of ODE Systems for Systems Biology,” Bioinformatics Advances, vol. 2, no. 2, 2022.
  20. Article
    RG1
    “A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column,” Journal of Automated Reasoning, vol. 66, 2022.
  21. Article
    RG1
    “Making Higher-Order Superposition Work,” Journal of Automated Reasoning, vol. 66, 2022.
  22. Article
    RG1
    “Extending a Brainiac Prover to Lambda-Free Higher-Order Logic,” International Journal on Software Tools for Technology Transfer (STTT), vol. 24, 2022.
  23. Article
    RG1
    “A Comprehensive Framework for Saturation Theorem Proving,” Journal of Automated Reasoning, vol. 66, 2022.

2021

  1. Article
    RG1
    “Superposition with Lambdas,” Journal of Automated Reasoning, vol. 65, 2021.
  2. Paper
    RG1
    “Superposition with Lambdas,” 2021. [Online]. Available: https://arxiv.org/abs/2102.00453.
  3. Article
    RG1
    “Superposition for Lambda-Free Higher-Order Logic,” Logical Methods in Computer Science, vol. 17, no. 2, 2021.
  4. Conference paper
    RG1
    “Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories,” in Verification, Model Checking, and Abstract Interpretation (VMCAI 2021), Copenhagen, Denmark (Online), 2021.
  5. Conference paper
    RG1
    “A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic,” in Frontiers of Combining Systems (FroCoS 2021), Birmingham, UK, 2021.
  6. Paper
    RG1
    “A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic,” 2021. [Online]. Available: https://arxiv.org/abs/2107.03189.
  7. Conference paper
    RG1
    “A Unifying Splitting Framework,” in Automated Deduction - CADE 28, Virtual Event, 2021.
  8. Article
    RG1
    “Foreword, with a Dedication to Andreas Weber,” Mathematics in Computer Science, vol. 15, 2021.
  9. Article
    RG1
    “Foreword, with a Dedication to Vladimir Gerdt,” Mathematics in Computer Science, vol. 15, 2021.
  10. Conference paper
    RG1
    “Termination of Polynomial Loops,” in Static Analysis (SAS 2020), Chicago, IL, USA (Online Event), 2021.
  11. Article
    RG1
    “Efficiently and Effectively Recognizing Toricity of Steady State Varieties,” Mathematics in Computer Science, vol. 15, 2021.
  12. Article
    RG1
    “Efficiently and Effectively Recognizing Toricity of Steady State Varieties,” Mathematics in Computer Science, vol. 15, 2021.
  13. Conference paper
    RG1
    “Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance,” in Automated Deduction - CADE 28, Virtual Event, 2021.
  14. Conference paper
    RG1
    “Abduction in EL via Translation to FOL,” in Second-Order Quantifier Elimination and Related Topics (SOQE 2021), Online Event, 2021.
  15. Article
    RG1
    “Algorithmic Reduction of Biological Networks With Multiple Time Scales,” Mathematics in Computer Science, vol. 15, 2021.
  16. Conference paper
    RG1
    “Superposition with First-class Booleans and Inprocessing Clausification,” in Automated Deduction - CADE 28, Virtual Event, 2021.
  17. Conference paper
    RG1
    “A Graph Theoretical Approach for Testing Binomiality of Reversible Chemical Reaction Networks,” in SYNASC 2020, 22nd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, 2021.
  18. Conference paper
    RG1
    “Parametric Toricity of Steady State Varieties of Reaction Networks,” in Computer Algebra in Scientific Computing (CASC 2021), Sochi, Russia, 2021.
  19. Paper
    RG1
    “Parametric Toricity of Steady State Varieties of Reaction Networks,” 2021. [Online]. Available: https://arxiv.org/abs/2105.10853.
  20. Paper
    RG1
    “Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gröbner Systems,” 2021. [Online]. Available: https://arxiv.org/abs/2107.01706.
  21. Conference paper
    RG1
    “Testing Binomiality of Chemical Reaction Networks Using Comprehensive Gröbner Systems,” in Computer Algebra in Scientific Computing (CASC 2021), Sochi, Russia, 2021.
  22. Conference paper
    RG1
    “Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant,” in Automated Deduction - CADE 28, Virtual Event, 2021.
  23. Article
    RG1
    “A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations,” Mathematics in Computer Science, vol. 15, 2021.
  24. Article
    RG1
    “The CADE-28 Automated Theorem Proving System Competition - CASC-28,” AI Communications, vol. 34, no. 4, 2021.
  25. Conference paper
    RG1
    “A Modular Isabelle Framework for Verifying Saturation Provers,” in CPP ’21, 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual, Denmark, 2021.
  26. Article
    RG1
    “Decidable ∃∗∀∗ First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates,” Journal of Automated Reasoning, vol. 65, 2021.
  27. Conference paper
    RG1
    “Making Higher-Order Superposition Work,” in Automated Deduction - CADE 28, Virtual Event, 2021.

2020

  1. Article
    RG1
    “Scalable Fine-Grained Proofs for Formula Processing,” Journal of Automated Reasoning, vol. 64, no. 3, 2020.
  2. Paper
    RG1
    “Superposition for Lambda-Free Higher-Order Logic,” 2020. [Online]. Available: https://arxiv.org/abs/2005.02094.
  3. Article
    RG1
    “Preface to the Special Issue on Automated Reasoning Systems,” Journal of Automated Reasoning, vol. 64, no. 3, 2020.
  4. Article
    RG1
    “Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks,” Journal of Symbolic Computation, vol. 98, 2020.
  5. Paper
    RG1
    “SCL with Theory Constraints,” 2020. [Online]. Available: https://arxiv.org/abs/2003.04627.
  6. Article
    RG1
    “A Complete and Terminating Approach to Linear Integer Solving,” Journal of Symbolic Computation, vol. 100, 2020.
  7. Article
    RG1
    “Symbolic Computation and Satisfiability Checking,” Journal of Symbolic Computation, vol. 100, 2020.
  8. Conference paper
    RG1
    “Towards Dynamic Dependable Systems Through Evidence-Based Continuous Certification,” in Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles, Rhodes, Greece (Virtual Event), 2020.
  9. Thesis
    RG1IMPR-CS
    “Formalization of Logical Calculi in Isabelle/HOL,” Universität des Saarlandes, Saarbrücken, 2020.
  10. Conference paper
    RG1
    “A Verified SAT Solver Framework including Optimization and Partial Valuations,” in LPAR-23, 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Virtual Conferernce, 2020.
  11. Paper
    RG1
    “A Calculus for Modular Loop Acceleration,” 2020. [Online]. Available: https://arxiv.org/abs/2001.01516.
  12. Article
    RG1
    “Inferring Lower Runtime Bounds for Integer Programs,” ACM Transactions on Programming Languages and Systems, vol. 42, 2020.
  13. Conference paper
    RG1
    “A Calculus for Modular Loop Acceleration,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Dublin, Ireland (Online Event), 2020.
  14. Conference paper
    RG1
    “On a Notion of Relevance,” in Proceedings of the 33rd International Workshop on Description Logics (DL 2020), Rhodes, Greece (Virtual Event), 2020.
  15. Conference paper
    RG1
    “Polynomial Loops: Beyond Termination,” in LPAR-23, 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Virtual Conferernce, 2020.
  16. Conference paper
    RG1
    “Signature-Based Abduction for Expressive Description Logics,” in Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), Rhodes, Greece (Virtual Conference), 2020.
  17. Paper
    RG1
    “Algorithmic Reduction of Biological Networks With Multiple Time Scales,” 2020. [Online]. Available: https://arxiv.org/abs/2010.10129.
  18. Conference paper
    RG1
    “A Linear Algebra Approach for Detecting Binomiality of Steady State Ideals of Reversible Chemical Reaction Networks,” in Computer Algebra in Scientific Computing (CASC 2020), Linz, Austria (Virtual Event), 2020.
  19. Paper
    RG1
    “A Graph Theoretical Approach for Testing Binomiality of Reversible Chemical Reaction Networks,” 2020. [Online]. Available: https://arxiv.org/abs/2010.12615.
  20. Conference paper
    RG1
    “First-Order Tests for Toricity,” in Computer Algebra in Scientific Computing (CASC 2020), Linz, Austria (Virtual Event), 2020.
  21. Paper
    RG1
    “First-Order Tests for Toricity,” 2020. [Online]. Available: https://arxiv.org/abs/2002.03586.
  22. Article
    RG1
    “Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover,” Journal of Automated Reasoning, vol. 64, 2020.
  23. Paper
    RG1
    “A Logic Based Approach to Finding Real Singularities of Implicit Ordinary Differential Equations,” 2020. [Online]. Available: https://arxiv.org/abs/2003.00740.
  24. Article
    RG1
    “SPASS-AR: A First-Order Theorem Prover Based on Approximation-Refinement into the Monadic Shallow Linear Fragment,” Journal of Automated Reasoning, vol. 64, no. 3, 2020.
  25. Conference paper
    RG1
    “A Comprehensive Framework for Saturation Theorem Proving,” in Automated Reasoning (IJCAR 2020), Paris, France (Virtual Conference), 2020.

2019

  1. Book chapter / section
    RG1
    “Hierarchic Superposition Revisited,” in Description Logic, Theory Combination, and All That, Berlin: Springer, 2019.
  2. Paper
    RG1
    “Hierarchic Superposition Revisited,” 2019. [Online]. Available: http://arxiv.org/abs/1904.03776.
  3. Article
    RG1
    “A Formal Proof of the Expressiveness of Deep Learning,” Journal of Automated Reasoning, vol. 63, no. 2, 2019.
  4. Conference paper
    RG1
    “Superposition with Lambdas,” in Automated Deduction -- CADE 27, Natal, Brazil, 2019.
  5. Article
    RG1
    “Bindings as Bounded Natural Functors,” Proceedings of the ACM on Programming Languages (Proc. POPL 2019), vol. 3, 2019.
  6. Conference paper
    RG1
    “Formalizing the Metatheory of Logical Calculi and Automatic Provers in Isabelle/HOL (Invited Talk),” in CPP’19, 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Cascais, Portugal, 2019.
  7. Paper
    RG1
    “Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks,” 2019. [Online]. Available: http://arxiv.org/abs/1902.04882.
  8. Thesis
    RG1IMPR-CS
    “Decision Procedures for Linear Arithmetic,” Universität des Saarlandes, Saarbrücken, 2019.
  9. Conference paper
    RG1
    “SPASS-SATT: A CDCL(LA) Solver,” in Automated Deduction -- CADE 27, Natal, Brazil, 2019.
  10. Article
    RG1
    “Logical Reduction of Metarules,” Machine Learning (Proc. ILP 2019), vol. 109, 2019.
  11. Conference paper
    RG1
    “SCL Clause Learning from Simple Models,” in Automated Deduction -- CADE 27, Natal, Brazil, 2019.
  12. Article
    RG1
    “Reconstructing veriT Proofs in Isabelle/HOL,” Electronic Proceedings in Theoretical Computer Science (Proc. PxTP 2019), no. 301, 2019.
  13. Conference paper
    RG1
    “Optimizing a Verified SAT Solver,” in NASA Formal Methods (NFM 2019), Houston, TX, USA, 2019.
  14. Paper
    RG1
    “Inferring Lower Runtime Bounds for Integer Programs,” 2019. [Online]. Available: https://arxiv.org/abs/1911.01077.
  15. Paper
    RG1
    “Proving Non-Termination via Loop Acceleration,” 2019. [Online]. Available: https://arxiv.org/abs/1905.11187.
  16. Conference paper
    RG1
    “Termination of Triangular Integer Loops is Decidable,” in Computer Aided Verification (CAV 2019), York City, NY, USA, 2019.
  17. Conference paper
    RG1
    “Proving Non-Termination via Loop Acceleration,” in Formal Methods in Computer Aided Design (FMCAD 2019), San Jose, CA, USA, 2019.
  18. Paper
    RG1
    “On the Decidability of Termination for Polynomial Loops,” 2019. [Online]. Available: https://arxiv.org/abs/1910.11588.
  19. Paper
    RG1
    “Termination of Triangular Integer Loops is Decidable,” 2019. [Online]. Available: https://arxiv.org/abs/1905.08664.
  20. Paper
    RG1
    “Efficiently and Effectively Recognizing Toricity of Steady State Varieties,” 2019. [Online]. Available: http://arxiv.org/abs/1910.04100.
  21. Conference paper
    RG1
    “A Verified Prover Based on Ordered Resolution,” in CPP’19, 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Cascais, Portugal, 2019.
  22. Conference paper
    RG1
    “On the Expressivity and Applicability of Model Representation Formalisms,” in Frontiers of Combining Systems (FroCos 2019), London, UK, 2019.
  23. Paper
    RG1
    “On the Expressivity and Applicability of Model Representation Formalisms,” 2019. [Online]. Available: http://arxiv.org/abs/1905.03651.
  24. Conference paper
    RG1
    “SLD-Resolution Reduction of Second-Order Horn Fragments,” in Logics in Artificial Intelligence (JELIA 2019), Rende, Italy, 2019.
  25. Thesis
    RG1IMPR-CS
    “Decidable Fragments of First-Order Logic and of First-Order Linear Arithmetic with Uninterpreted Predicates,” Universität des Saarlandes, Saarbrücken, 2019.
  26. Paper
    RG1
    “Separateness of Variables - A Novel Perspective on Decidable First-Order Fragments,” 2019. [Online]. Available: http://arxiv.org/abs/1911.11500.
  27. Conference paper
    RG1
    “Extending a Brainiac Prover to Lambda-Free Higher-Order Logic,” in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Prague, Czech Republic, 2019.
  28. Article
    RG1
    “The Challenge of Unifying Semantic and Syntactic Inference Restrictions,” Electronic Proceedings in Theoretical Computer Science (Proc. ARCADE 2019), vol. 311, 2019.

2018

  1. Article
    RG1
    “A Machine-checked Correctness Proof for Pastry,” Science of Computer Programming, vol. 158, 2018.
  2. Conference paper
    RG1
    “Superposition for Lambda-Free Higher-Order Logic,” in Automated Reasoning (IJCAR 2018), Oxford, UK, 2018.
  3. Article
    RG1
    “A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality,” Journal of Automated Reasoning, vol. 61, no. 1–4, 2018.
  4. Conference paper
    RG1
    “Superposition with Datatypes and Codatatypes,” in Automated Reasoning (IJCAR 2018), Oxford, UK, 2018.
  5. Article
    RG1
    “The SYMBIONT Project: Symbolic Methods for Biological Networks,” Faculty of 1000 Research, vol. 7, 2018.
  6. Article
    RG1
    “The SYMBIONT Project: Symbolic Methods for Biological Networks,” ACM Communications in Computer Algebra, vol. 52, no. 3, 2018.
  7. Conference paper
    RG1
    “A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems,” in Automated Reasoning (IJCAR 2018), Oxford, UK, 2018.
  8. Conference paper
    RG1
    “Derivation Reduction of Metarules in Meta-interpretive Learning,” in Inductive Logic Programming (ILP 2018), Ferrara, Italy, 2018.
  9. Conference paper
    RG1
    “Prime Implicate Generation in Equational Logic,” in Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI 2018), Stockholm, Sweden, 2018.
  10. Conference paper
    RG1
    “A Verified SAT Solver with Watched Literals using Imperative HOL,” in CPP’18, 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Los Angeles, CA, USA, 2018.
  11. Conference paper
    RG1
    “Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT,” in Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation co-located with Federated Logic Conference (SC-Square 2018), Oxford, UK, 2018.
  12. Paper
    RG1
    “Positive Solutions of Systems of Signed Parametric Polynomial Inequalities,” 2018. [Online]. Available: http://arxiv.org/abs/1804.09705.
  13. Conference paper
    RG1
    “Positive Solutions of Systems of Signed Parametric Polynomial Inequalities,” in Computer Algebra in Scientific Computing (CASC 2018), Lille, France, 2018.
  14. Conference paper
    RG1
    “Formalizing of Bachmair and Ganzinger’s Ordered Resolution Prover,” in Automated Reasoning (IJCAR 2018), Oxford, UK, 2018.
  15. Article
    RG1
    “Formalization of Bachmair and Ganzinger’s Ordered Resolution Prover,” Archive of Formal Proofs, 2018.
  16. Conference paper
    RG1
    “Thirty Years of Virtual Substitution: Foundations, Techniques, Applications,” in ISSAC’18, 43rd International Symposium on Symbolic and Algebraic Computation, New York, NY, USA, 2018.
  17. Thesis
    RG1IMPR-CS
    “An Approximation and Refinement Approach to First-Order Automated Reasoning,” Universität des Saarlandes, Saarbrücken, 2018.

2017

  1. Article
    D1RG1
    “Verification of Linear Hybrid Systems with Large Discrete State Spaces Using Counterexample-guided Abstraction Refinement,” Science of Computer Programming, vol. 148, 2017.
  2. Article
    RG1
    “Language and Proofs for Higher-Order SMT (Work in Progress),” Electronic Proceedings in Theoretical Computer Science, vol. 262, 2017.
  3. Conference paper
    RG1
    “Scalable Fine-Grained Proofs for Formula Processing,” in Automated Deduction -- CADE 26, Gothenburg, Sweden, 2017.
  4. Article
    RG1
    “Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings,” Journal of Symbolic Computation, vol. 81, 2017.
  5. Conference paper
    RG1
    “A Transfinite Knuth–Bendix Order for Lambda-Free Higher-Order Terms,” in Automated Deduction -- CADE 26, Gothenburg, Sweden, 2017.
  6. Conference paper
    RG1
    “A Formal Proof of the Expressiveness of Deep Learning,” in Interactive Theorem Proving (ITP 2017), Brasilia, Brazil, 2017.
  7. Conference paper
    RG1
    “Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic,” in Frontiers of Combining Systems (FroCoS 2017), Brasília, Brazil, 2017.
  8. Article
    RG1
    “Soundness and Completeness Proofs by Coinductive Methods,” Journal of Automated Reasoning, vol. 58, no. 1, 2017.
  9. Article
    RG1
    “Abstract Soundness,” Archive of Formal Proofs, 2017.
  10. Conference paper
    RG1
    “A Lambda-Free Higher-Order Recursive Path Order,” in Foundations of Software Science and Computation Structures (FoSSaCS 2017), Uppsala, Sweden, 2017.
  11. Conference paper
    RG1
    “A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality,” in Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI 2017), Melbourne, Australia, 2017.
  12. Conference paper
    RG1
    “Towards Strong Higher-Order Automation for Fast Interactive Verification,” in ARCADE 2017, Gothenburg, Sweden, 2017.
  13. Conference paper
    RG1
    “Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL,” in 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Oxford, UK, 2017.
  14. Conference paper
    RG1
    “A Case Study on the Parametric Occurrence of Multiple Steady States,” in ISSAC’17, International Symposium on Symbolic and Algebraic Computation, Kaiserslautern, Germany, 2017.
  15. Paper
    RG1
    “A Case Study on the Parametric Occurrence of Multiple Steady States,” 2017. [Online]. Available: http://arxiv.org/abs/1704.08997.
  16. Article
    RG1
    “New Techniques for Linear Arithmetic: Cubes and Equalities,” Formal Methods in System Design, vol. 51, no. 3, 2017.
  17. Article
    RG1
    “Preface -Special Issue of Selected Extended Papers of IJCAR 2014,” Journal of Automated Reasoning, vol. 58, no. 1, 2017.
  18. Article
    RG1
    “Prime Implicate Generation in Equational Logic,” Journal of Artificial Intelligence Research, vol. 60, 2017.
  19. Paper
    RG1
    “Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks,” 2017. [Online]. Available: http://arxiv.org/abs/1706.08794.
  20. Conference paper
    RG1
    “Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks,” in Computer Algebra in Scientific Computing, Beijing, China, 2017.
  21. Paper
    RG1
    “Subtropical Satisfiability,” 2017. [Online]. Available: http://arxiv.org/abs/1706.09236.
  22. Conference paper
    RG1
    “Subtropical Satisfiability,” in Frontiers of Combining Systems (FroCoS 2017), Brasília, Brazil, 2017.
  23. Paper
    RG1
    “On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic,” 2017. [Online]. Available: http://arxiv.org/abs/1705.08792.
  24. Conference paper
    RG1
    “On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic,” in Automated Deduction -- CADE 26, Gothenburg, Sweden, 2017.
  25. Paper
    RG1
    “The Universal Fragment of Presburger Arithmetic with Unary Uninterpreted Predicates is Undecidable,” 2017. [Online]. Available: http://arxiv.org/abs/1703.01212.
  26. Article
    RG1
    “BDI: A New Decidable Clause Class,” Journal of Logic and Computation, vol. 27, no. 2, 2017.
  27. Article
    RG1
    “A Decision Procedure for (Co)datatypes in SMT Solvers,” Journal of Automated Reasoning, vol. 58, no. 3, 2017.
  28. Article
    RG1
    “A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications,” Mathematics in Computer Science, vol. 11, no. 3–4, 2017.
  29. Thesis
    RG1IMPR-CS
    “Logics for Rule-based Configuration Systems,” Universität des Saarlandes, Saarbrücken, 2017.
  30. Paper
    RG1
    “Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints,” 2017. [Online]. Available: http://arxiv.org/abs/1703.02837.
  31. Conference paper
    RG1
    “Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints,” in Automated Deduction -- CADE 26, Gothenburg, Sweden, 2017.
  32. Conference paper
    RG1
    “The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable,” in Frontiers of Combining Systems (FroCoS 2017), Brasília, Brazil, 2017.
  33. Conference paper
    RG1
    “A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment,” in 32nd Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2017), Reykjavik, Iceland, 2017.
  34. Paper
    RG1
    “The Bernays-Schönfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable,” 2017. [Online]. Available: http://arxiv.org/abs/1706.08504.
  35. Paper
    RG1
    “On Generalizing Decidable Standard Prefix Classes of First-Order Logic,” 2017. [Online]. Available: http://arxiv.org/abs/1706.03949.
  36. Conference paper
    RG1
    “Towards Elimination of Second-Order Quantifiers in the Separated Fragment,” in Proceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE 2017), Dresden, Germany, 2017.
  37. Paper
    RG1
    “A Fine-Grained Hierarchy of Hard Problems in the Separated Fragment,” 2017. [Online]. Available: http://arxiv.org/abs/1704.02145.
  38. Thesis
    RG1IMPR-CS
    “Superposition: Types and Induction,” Universität des Saarlandes, Saarbrücken, 2017.
  39. Conference paper
    RG1
    “Do Portfolio Solvers Harm?,” in ARCADE 2017, Gothenburg, Sweden, 2017.

2016

  1. Paper
    RG1
    “SC2: Satisfiability Checking meets Symbolic Computation (Project Paper),” 2016. [Online]. Available: http://arxiv.org/abs/1607.08028.
  2. Conference paper
    RG1
    “SC2: Satisfiability Checking Meets Symbolic Computation,” in Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, 2016.
  3. Article
    RG1
    “Satisfiability Checking and Symbolic Computation,” ACM Communications in Computer Algebra, vol. 50, no. 4, 2016.
  4. Paper
    RG1
    “Satisfiability Checking and Symbolic Computation,” 2016. [Online]. Available: http://arxiv.org/abs/1607.06945.
  5. Report
    D1RG1IMPR-CS
    “Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization,” SFB/TR 14 AVACS, ATR103, 2016.
  6. Thesis
    RG1IMPR-CS
    “A Machine-checked Proof of Correctness of Pastry,” Universität des Saarlandes, Saarbrücken, 2016.
  7. Conference paper
    RG1
    “A Rigorous Correctness Proof for Pastry,” in Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016), Linz, Austria, 2016.
  8. Article
    RG1
    “Encoding Monomorphic and Polymorphic Types,” Logical Methods in Computer Science, vol. 12, no. 4, 2016.
  9. Proceedings
    RG1
    Eds., Proceedings First International Workshop on Hammers for Type Theories. EPTCS, 2016.
  10. Article
    RG1
    “Hammering towards QED,” Journal of Formalized Reasoning, vol. 9, no. 1, 2016.
  11. Paper
    RG1
    “Encoding Monomorphic and Polymorphic Types,” 2016. [Online]. Available: http://arxiv.org/abs/1609.08916.
  12. Conference paper
    RG1
    “A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality,” in Automated Reasoning (IJCAR 2016), Coimbra, Portugal, 2016.
  13. Article
    RG1
    “Semi-intelligible Isar Proofs from Machine-Generated Proofs,” Journal of Automated Reasoning, vol. 56, no. 2, 2016.
  14. Article
    RG1
    “A Learning-Based Fact Selector for Isabelle/HOL,” Journal of Automated Reasoning, vol. 57, no. 3, 2016.
  15. Proceedings
    RG1
    Eds., Interactive Theorem Proving. Springer, 2016.
  16. Thesis
    RG1
    “Analysis and Implementation of LIA solvers: CutSAT and BBSAT,” Universität des Saarlandes, Saarbrücken, 2016.
  17. Conference paper
    RG1
    “Computing a Complete Basis for Equalities Implied by a System of LRA Constraints,” in Satisfiability Modulo Theories (SMT 2016), Coimbra, Portugal, 2016.
  18. Conference paper
    RG1
    “Fast Cube Tests for LIA Constraint Solving,” in Automated Reasoning (IJCAR 2016), Coimbra, Portugal, 2016.
  19. Conference paper
    RG1
    “Extending Nunchaku to Dependent Type Theory,” in Proceedings First International Workshop on Hammers for Type Theories (HaTT 2016), Coimbra, Portugal, 2016.
  20. Conference paper
    RG1
    “Compliance, Functional Safety and Fault Detection by Formal Methods,” in Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), Corfu, Greece, 2016.
  21. Thesis
    RG1IMPR-CS
    “New Concepts for Real Quantifier Elimination by Virtual Substitution,” Universität des Saarlandes, Saarbrücken, 2016.
  22. Article
    RG1
    “Better Answers to Real Questions,” Journal of Symbolic Computation, vol. 74, 2016.
  23. Conference paper
    RG1
    “A Decision Procedure for (Co)datatypes in SMT Solvers,” in Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI 2016), New York, NY, USA, 2016.
  24. Conference paper
    RG1
    “Model Finding for Recursive Functions in SMT,” in Automated Reasoning (IJCAR 2016), Coimbra, Portugal, 2016.
  25. Conference paper
    RG1
    “Deciding First-Order Satisfiability when Universal and Existential Variables are Separated,” in Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016), New York, NY, USA, 2016.
  26. Paper
    RG1
    “Deciding First-Order Satisfiability when Universal and Existential Variables are Separated,” 2016. [Online]. Available: http://arxiv.org/abs/1511.08999.
  27. Conference paper
    RG1
    “A Dynamic Logic for Configuration,” in Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, 2016.
  28. Conference paper
    RG1
    “Ordered Resolution with Straight Dismatching Constraints,” in Practical Aspects of Automated Reasoning (PAAR 2016), Coimbra, Portugal, 2016.
  29. Conference paper
    RG1
    “The Complexity of Satisfiability in the Separated Fragment - A Journey Through ELEMENTARY and Beyond,” in Seventeenth International Workshop on Logic and Computational Complexity (LCC 2016), Marseille, France, 2016.
  30. Conference paper
    RG1
    “Beyond Standard Miniscoping,” in Deduktionstreffen 2016, Klagenfurt, Austria, 2016.
  31. Thesis
    RG1
    “More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification,” Universität des Saarlandes, Saarbrücken, 2016.

2015

  1. Conference paper
    RG1
    “NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment,” in Frontiers of Combining Systems (FroCoS 2015), Wrocław, Poland, 2015.
  2. Paper
    RG1
    “NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment,” 2015. [Online]. Available: http://arxiv.org/abs/1502.05501.
  3. Paper
    RG1
    “Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings,” 2015. [Online]. Available: http://arxiv.org/abs/1511.00180.
  4. Conference paper
    RG1
    “Beagle -- A Hierarchic Superposition Theorem Prover,” in Automated Deduction -- CADE-25, Berlin, Germany, 2015.
  5. Conference paper
    RG1
    “Mining the Archive of Formal Proofs,” in Intelligent Computer Mathematics (CICM 2015), Washington, DC, USA, 2015.
  6. Conference paper
    RG1
    “Foundational Extensible Corecursion: A Proof Assistant Perspective,” in ACM SIGPLAN Notices (Proc. ICFP 2015), Vancouver, BC, Canada, 2015, vol. 50, no. 9.
  7. Proceedings
    RG1
    Eds., Tests and Proofs. Springer, 2015.
  8. Conference paper
    RG1
    “Witnessing (Co)datatypes,” in Programming Languages and Systems (ESOP 2015), London, UK, 2015.
  9. Paper
    RG1
    “Foundational Extensible Corecursion,” 2015. [Online]. Available: http://arxiv.org/abs/1501.05425.
  10. Paper
    RG1
    “Linear Integer Arithmetic Revisited,” 2015. [Online]. Available: http://arxiv.org/abs/1503.02948.
  11. Conference paper
    RG1
    “Linear Integer Arithmetic Revisited,” in Automated Deduction -- CADE-25, Berlin, Germany, 2015.
  12. Article
    RG1
    “Constructing a Single Cell in Cylindrical Algebraic Decomposition,” Journal of Symbolic Computation, vol. 70, 2015.
  13. Conference paper
    RG1
    “Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata,” in Frontiers of Combining Systems (FroCoS 2015), Wrocław, Poland, 2015.
  14. Report
    RG1
    “Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata,” SFB/TR 14 AVACS, ATR111, 2015.
  15. Article
    RG1
    “Detection of Hopf Bifurcations in Chemical Reaction Networks Using Convex Coordinates,” Journal of Computational Physics, vol. 291, 2015.
  16. Article
    RG1
    “Foreword to the Special Focus on Constraints and Combinations,” Mathematics in Computer Science, vol. 9, no. 3, 2015.
  17. Thesis
    RG1IMPR-CS
    “Symbolic Orthogonal Projections: A New Polyhedral Representation for Reachability Analysis of Hybrid Systems,” Universität des Saarlandes, Saarbrücken, 2015.
  18. Paper
    RG1
    “Optimising Spatial and Tonal Data for PDE-based Inpainting,” 2015. [Online]. Available: http://arxiv.org/abs/1506.04566.
  19. Conference paper
    RG1
    “Adapting Real Quantifier Elimination Methods for Conflict Set Computation,” in Frontiers of Combining Systems (FroCoS 2015), Wrocław, Poland, 2015.
  20. Conference paper
    RG1
    “Model-Based Variant Management with v.control,” in Transdisciplinary Lifecycle Analysis of Systems (ISPE CE 2015), Delft, The Netherlands, 2015.
  21. Book chapter / section
    RG1
    “Ore Polynomials in Sage,” in Computer Algebra and Polynomials, Berlin: Springer, 2015.
  22. Conference paper
    RG1
    “What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead,” in 24th EACSL Annual Conference on Computer Science Logic, Berlin, Germany, 2015.
  23. Conference paper
    RG1
    “How Much Lookahead is Needed to Win Infinite Games?,” in Automata, Languages, and Programming (ICALP 2015), Kyoto, Japan, 2015.
  24. Paper
    RG1
    “A Generalized Framework for Virtual Substitution,” 2015. [Online]. Available: http://arxiv.org/abs/1501.05826.
  25. Paper
    RG1
    “Better Answers to Real Questions,” 2015. [Online]. Available: http://arxiv.org/abs/1501.05098.
  26. Thesis
    RG1IMPR-CS
    “Automatic Authorization Analysis,” Universität des Saarlandes, Saarbrücken, 2015.
  27. Conference paper
    RG1
    “A Decision Procedure for (Co)datatypes in SMT Solvers,” in Automated Deduction -- CADE-25, Berlin, Germany, 2015.
  28. Report
    RG1
    “Modal Tableau Systems with Blocking and Congruence Closure,” University of Manchester, Manchester, uk-ac-man-scw:268816, 2015.
  29. Conference paper
    RG1
    “Modal Tableau Systems with Blocking and Congruence Closure,” in Automated Reasoning with Analytic Tableaux and Related Methods, Wrocław, Poland, 2015.
  30. Conference paper
    RG1
    “Hierarchical Reasoning in Local Theory Extensions and Applications,” in SYNASC 2014, Timisoara, Romania, 2015.