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.
  31. Paper
    RG1
    “Subtropical Real Root Finding,” 2015. [Online]. Available: http://arxiv.org/abs/1501.04836.
  32. Conference paper
    RG1
    “Subtropical Real Root Finding,” in ISSAC’15, 40th International Symposium on Symbolic and Algebraic Computation, Bath, UK, 2015.
  33. Thesis
    RG1IMPR-CS
    “Resolution-based Methods for Linear Temporal Reasoning,” Universität des Saarlandes, Saarbrücken, 2015.
  34. Article
    RG1
    “Variable and Clause Elimination for LTL Satisfiability Checking,” Mathematics in Computer Science, vol. 9, no. 3, 2015.
  35. Conference paper
    RG1
    “First-order Logic Theorem Proving and Model Building via Approximation and Instantiation,” in Frontiers of Combining Systems (FroCoS 2015), Wrocław, Poland, 2015.
  36. Paper
    RG1
    “First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation,” 2015. [Online]. Available: http://arxiv.org/abs/1503.02971.
  37. Paper
    RG1
    “Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete,” 2015. [Online]. Available: http://arxiv.org/abs/1501.07209.
  38. Conference paper
    RG1
    “Automated Reasoning Building Blocks,” in Correct System Design, Oldenburg, Germany, 2015.

2014

  1. Conference paper
    RG1
    “Finite Quantification in Hierarchic Theorem Proving,” in Automated Reasoning (IJCAR 2014), Vienna, Austria, 2014.
  2. Proceedings
    RG1
    Eds., Deduction and Arithmetic, no. 10. Schloss Dagstuhl, 2014.
  3. Proceedings
    RG1
    Eds., Automated Reasoning. Springer, 2014.
  4. Thesis
    RG1IMPR-CS
    “Labelled Superposition,” Universität des Saarlandes, Saarbrücken, 2014.
  5. Proceedings
    RG1
    Eds., Automated Deduction: Decidability, Complexity, Tractability. Universität Koblenz, 2014.
  6. Report
    RG1
    “Obtaining Finite Local Theory Axiomatizations via Saturation,” SFB/TR 14 AVACS, ATR93, 2014.
  7. Conference paper
    RG1
    “Locality Transfer: From Constrained Axiomatizations to Reachability Predicates,” in Automated Reasoning (IJCAR 2014), Vienna, Austria, 2014.
  8. Conference paper
    RG1
    “Towards Conflict-driven Learning for Virtual Substitution,” in 12th International Workshop on Satisfiability Modulo Theories (SMT 2014), Vienna, Austria, 2014.
  9. Conference paper
    RG1
    “Towards Conflict-driven Learning for Virtual Substitution,” in Computer Algebra in Scientific Computing (CASC 2014), Warsaw, Poland, 2014.
  10. Conference paper
    RG1
    “Better Answers to Real Questions,” in 12th International Workshop on Satisfiablity Modulo Theories (SMT 2014), Vienna, Austria, 2014.
  11. Conference paper
    RG1
    “Bisimulations and Logical Characterizations on Continuous-time Markov Decision Processes,” in Verification, Model Checking, and Abstract Interpretation (VMCAI 2014), San Diego, CA, USA, 2014.
  12. Article
    RG1
    “Property Directed Reachability for Automated Planning,” Journal of Artificial Intelligence Research, vol. 50, 2014.
  13. Conference paper
    RG1
    “Polymorphic+Typeclass Superposition,” in 4th Workshop on Practical Aspects of Automated Reasoning (PAAR 2014), Vienna, Austria, 2014.

2013

  1. Conference paper
    RG1
    “Computing Tiny Clause Normal Forms,” in Automated Deduction - CADE-24, Lake Placid, NY, USA, 2013, vol. 7898.
  2. Conference paper
    RG1
    “Hierarchic Superposition: Completeness without Compactness,” in Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences (MACIS 2013), Nanning, China, 2013.
  3. Report
    RG1
    “Hierarchic Superposition with Weak Abstraction,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-2014-RG1-002, 2013.
  4. Conference paper
    RG1
    “Hierarchic Superposition with Weak Abstraction,” in Automated Deduction - CADE-24, Lake Placid, NY, USA, 2013.
  5. Article
    RG1
    “Preface: Special Issue of Selected Extended Papers of CADE-23,” Journal of Automated Reasoning, vol. 51, no. 1, 2013.
  6. Conference paper
    RG1
    “Automated Verification of Interactive Rule-based Configuration Systems,” in 28th IEEE/ACM International Conference on Automated Software Engineering (ASE 2013), Palo Alto, CA, USA, 2013.
  7. Book chapter / section
    RG1
    “Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates,” in Computer Algebra in Scientific Computing, Berlin: Springer, 2013.
  8. Thesis
    RG1
    “Computing Variable Orders for SAT-Problems,” Universität des Saarlandes, Saarbrücken, 2013.
  9. Article
    RG1
    “Superposition as a Decision Procedure for Timed Automata,” Mathematics in Computer Science, vol. 6, no. 4, 2013.
  10. Proceedings
    RG1
    Eds., Automated Deduction: Decidability, Complexity, Tractability. 2013.
  11. Book chapter / section
    RG1
    “From Search to Computation: Redundancy Criteria and Simplification at Work,” in Programming Logics, Berlin: Springer, 2013.
  12. Book chapter / section
    RG1
    “Superposition for Bounded Domains,” in Automated Reasoning and Mathematics, Berlin: Springer, 2013.
  13. Conference paper
    RG1
    “Obtaining Finite Local Theory Axiomatizations via Saturation,” in Frontiers of Combining Systems (FroCoS 2013), Nancy, France, 2013.
  14. Proceedings
    RG1
    INFORMATIK 2013 - Informatik angepasst an Mensch, Organisation und Umwelt. Köllen, 2013.
  15. Book chapter / section
    RG1
    “Harald Ganzinger’s Legacy: Contributions to Logics and Programming,” in Programming Logics, Berlin: Springer, 2013.
  16. Conference paper
    RG1
    “Presburger Arithmetic in Memory Access Optimization for Data-parallel Languages,” in Frontiers of Combining Systems (FroCoS 2013), Nancy, France, 2013.
  17. Conference paper
    RG1
    “SMT-based Compiler Support for Memory Access Optimization for Data-parallel Languages,” in Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences (MACIS 2013), Nanning, China, 2013.
  18. Proceedings
    RG1
    Eds., Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and Information Sciences. 2013.
  19. Thesis
    RG1IMPR-CSD1
    “Superposition Modulo Theory,” Universität des Saarlandes, Saarbrücken, 2013.
  20. Conference paper
    RG1
    “BDI: A New Decidable First-order Clause Class,” in LPAR-19, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Stellenbosch, South Africa, 2013.
  21. Thesis
    RG1IMPR-CS
    “Formal Verification of the Pastry Protocol,” Universität des Saarlandes, Saarbrücken, 2013.
  22. Thesis
    RG1
    “Real Linear Quantifier Elimination,” Universität des Saarlandes, Saarbrücken, 2013.
  23. Conference paper
    RG1
    “Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems,” in Automated Deduction - CADE-24, Lake Placid, NY, USA, 2013.
  24. Book chapter / section
    RG1
    “On Combinations of Local Theory Extensions,” in Programming Logics, Berlin: Springer, 2013.
  25. Article
    RG1
    “Locality and Applications to Subsumption Testing in EL and Some of its Extensions,” Scientific Annals of Computer Science, vol. 23, no. 2, 2013.
  26. Conference paper
    RG1
    “Variable and Clause Elimination for LTL Satisfiability Checking,” in Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences (MACIS 2013), Nanning, China, 2013.
  27. Paper
    RG1
    “Triggered Clause Pushing for IC3,” 2013. [Online]. Available: http://arxiv.org/abs/1307.4966.
  28. Thesis
    RG1
    “CDCL with Reduction,” Universität des Saarlandes, Saarbrücken, 2013.
  29. Book
    RG1
    Eds., Programming Logics. Berlin: Springer, 2013.

2012

  1. Thesis
    RG1IMPR-CS
    “Formula Renaming with Generalizations,” Universität des Saarlandes, Saarbrücken, 2012.
  2. Conference paper
    RG1
    “More SPASS with Isabelle : Superposition with Hard Sorts and Configurable Simplification,” in Interactive Theorem Proving (ITP 2012), Princeton, NJ, 2012.
  3. Thesis
    RG1
    “Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic,” Universität des Saarlandes, Saarbrücken, 2012.
  4. Article
    RG1
    “Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces,” Science of Computer Programming, vol. 77, 2012.
  5. Report
    RG1
    “Automatic Generation of Invariants for Circular Derivations in SUP(LA) 1,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-2012-RG1-002, 2012.
  6. Conference paper
    RG1
    “Automatic Generation of Invariants for Circular Derivations in SUP(LA),” in Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2012), Mérida, Venezuela, 2012.
  7. Conference paper
    RG1
    “Combination of Disjoint Theories: Beyond Decidability,” in Automated Reasoning, Machnester, UK, 2012.
  8. Article
    RG1
    “Superposition Decides the First-order Logic Fragment Over Ground Theories,” Mathematics in Computer Science, vol. 6, no. 4, 2012.
  9. Article
    RG1
    “First-order Theorem Proving: Foreword,” Journal of Symbolic Computation, vol. 47, no. 9, 2012.
  10. Conference paper
    RG1
    “A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance,” in Automated Reasoning (IJCAR 2012), Manchester, UK, 2012.
  11. Report
    RG1
    “Labelled Superposition for PLTL,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-2012-RG1-001, 2012.
  12. Conference paper
    RG1
    “Labelled Superposition for PLTL,” in Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2012), Mérida, Venezuela, 2012.
  13. Conference paper
    RG1
    “Satisfiability Checking and Query Answering for Large Ontologies,” in PAAR-2012, Third Workshop on Practical Aspects of Automated Reasoning, Manchester, UK, 2012.
  14. Thesis
    RG1IMPR-CSD5
    “Efficient Reasoning Procedures for Complex First-order Theories,” Universität des Saarlandes, Saarbrücken, 2012.

2011

  1. Article
    RG1
    “A Combined Superposition and Model Evolution Calculus,” Journal of Automated Reasoning, vol. 47, no. 2, 2011.
  2. Proceedings
    RG1
    Eds., Automated Deduction - CADE-23 : 23rd International Conference on Automated Deduction. Springer, 2011.
  3. Article
    RG1
    “Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo,” Logical Methods in Computer Science, vol. 7, no. 1, 2011.
  4. Article
    RG1
    “PTIME parametric verification of safety properties for reasonable linear hybrid automata,” Mathematics in Computer Science, vol. 5, no. 4, 2011.
  5. Conference paper
    RG1
    “Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata,” in HSCC’11 : Proceedings of the 2011 ACM/SIGBED Hybrid Systems: Computation and Control, 2011.
  6. Report
    RG1
    “PTIME Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata,” SFB/TR 14 AVACS, ATR70, 2011.
  7. Report
    RG1
    “Integrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems,” SFB/TR 14 AVACS, Saarbrücken, ATR76, 2011.
  8. Conference paper
    RG1
    “Superposition Modulo Non-linear Arithmetic,” in Frontiers of Combining Systems (FroCoS 2011), Saarbruecken, Germany, 2011.
  9. Conference paper
    RG1
    “Efficient TBox Subsumption Checking in Combinations of EL and (fragments of) FL0,” in Proceedings of the 2011 International Workshop on Description Logics (DL-2011), 2011.
  10. Conference paper
    RG1
    “Automatic Verification of the Adequacy of Models for Families of Geometric Objects,” in Automated Deduction in Geometry (ADG 2008), Shanghai, China, 2011.
  11. Conference paper
    RG1
    “Towards Verification of the Pastry Routing Protocol using TLA+,” in Formal Techniques for Distributed Systems (FMOODS 2011), Reykjavik, Iceland, 2011.
  12. Report
    RG1
    “Towards Verification of the Pastry Protocol using TLA+,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-2011-RG1-002, 2011.
  13. Conference paper
    RG1
    “Verification and Synthesis Using Real Quantifier Elimination,” in ISSAC 2011, San Jose, CA, 2011.
  14. Proceedings
    RG1
    Eds., Automated Deduction in Geometry : 7th International Workshop, ADG 2008. Springer, 2011.
  15. Proceedings
    RG1
    Eds., Frontiers of Combining Systems. Springer, 2011.
  16. Article
    RG1
    “Algorithmic Global Criteria for Excluding Oscillations,” Bulletin of Mathematical Biology, vol. 73, no. 4, 2011.

2010

  1. Conference paper
    RG1
    “Embedding Deduction Modulo into a Prover,” in Computer Science Logic (CSL 2010), Brno, Czech Republic, 2010.
  2. Conference paper
    RG1
    “Automatic Verification of Parametric Specifications with Complex Topologies,” in Integrated Formal Methods (IFM 2010), Nancy, France, 2010.
  3. Report
    RG1
    “Automatic Verification of Parametric Specifications with Complex Topologies,” SFB/TR 14 AVACS, ATR66, 2010.
  4. Conference paper
    RG1
    “Superposition-Based Analysis of First-Order Probabilistic Timed Automata,” in Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2010), Yogyakarta, Indonesia, 2010.
  5. Article
    RG1
    “Special Issue on Automated Deduction: Decidability, complexity, tractability,” Journal of Symbolic Computation, vol. 45, no. 2, 2010.
  6. Article
    RG1
    “Superposition for Fixed Domains,” ACM Transactions on Computational Logic, vol. 11, no. 4, 2010.
  7. Conference paper
    RG1
    “Disunification for Ultimately Periodic Interpretations,” in Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2010), Dakar, Senegal, 2010.
  8. Thesis
    RG1IMPR-CS
    “Saturation-based Decision Procedures for Fixed Domain and Minimal Model Semantics,” Universität des Saarlandes, Saarbrücken, 2010.
  9. Thesis
    RG1IMPR-CS
    “Reasoning in Combinations of Theories,” Universität des Saarlandes, Saarbrücken, 2010.
  10. Conference paper
    RG1
    “On Hierarchical Reasoning in Combinations of Theories,” in Automated Reasoning (IJCAR 2010), Edinburgh, UK, 2010.
  11. Report
    RG1
    “On Hierarchical Reasoning in Combinations of Theories,” SFB/TR 14 AVACS, ATR60, 2010.
  12. Report
    RG1
    “System Description: H-PILoT (Version 1.9),” SFB/TR 14 AVACS, ATR61, 2010.
  13. Thesis
    RG1IMPR-CS
    “Hierarchic Decision Procedures for Verification,” Universität des Saarlandes, Saarbrücken, 2010.
  14. Conference paper
    RG1
    “Model Checking the Pastry Routing Protocol,” in Proceedings of the 10th International Workshop Automatic Verification of Critical Systems (AVOCS 2010), Düsseldorf, Germany, 2010.
  15. Proceedings
    RG1
    Eds., FTP 2009 First-Order Theorem Proving. CEUR- WS.org, 2010.
  16. Article
    RG1
    “Constraint Solving for Interpolation,” Journal of Symbolic Computation, vol. 45, no. 11, 2010.
  17. Conference paper
    RG1
    “Automated Reasoning in Extensions of Theories of Constructors with Recursively Defined Functions and Homomorphisms,” in Interaction versus Automation : the two Faces of Deduction, Schloss Dagstuhl, Wadern, 2010.
  18. Conference paper
    RG1
    “Hierarchical Reasoning for the Verification of Parametric Systems,” in Automated Reasoning (IJCAR 2010), Edinburgh, UK, 2010.
  19. Conference paper
    RG1
    “On the Saturation of YAGO,” in Automated Reasoning (IJCAR 2010), Edinburgh, UK, 2010.
  20. Report
    RG1
    “On the saturation of YAGO,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-2010-RG1-001, 2010.
  21. Conference paper
    RG1D5
    “Progress Towards Effective Automated Reasoning with World Knowledge,” in Proceedings of the Twenty-Third International Florida Artificial Intelligence Research Society Conference (FLAIRS 2010), Daytona Beach, FL, USA, 2010.
  22. Article
    RG1
    “Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation,” Journal of Symbolic Computation, vol. 45, no. 2, 2010.
  23. Article
    RG1
    “Subterm Contextual Rewriting,” AI Communications, vol. 23, no. 2–3, 2010.

2009

  1. Conference paper
    D1RG1
    “Superposition Modulo Linear Arithmetic SUP(LA),” in Frontiers of Combining Systems (FroCos 2009), Trento, Italy, 2009.
  2. Conference paper
    RG1
    “Superposition and Model Evolution Combined,” in Automated Deduction, CADE-22, 22nd International Conference on Automated Deduction, 2009.
  3. Thesis
    RG1
    “On the Translation of Timed Automata into First-order Logic,” Universität des Saarlandes, Saarbrücken, 2009.
  4. Thesis
    RG1
    “Automatic Analysis of Tree-Based Feature Models with SPASS,” Universität des Saarlandes, Saarbrücken, 2009.
  5. Article
    RG1
    “Labelled Splitting,” Annals of Mathematics and Artificial Intelligence, vol. 55, no. 1–2, 2009.
  6. Conference paper
    RG1
    “Deciding the Inductive Validity of FOR ALL THERE EXISTS * Queries,” in CSL, 2009.
  7. Conference paper
    RG1
    “Decidability Results for Saturation-Based Model Building,” in 22nd International Conference on Automated Deduction (CADE-22), 2009.
  8. Report
    RG1
    “Deciding the Inductive Validity of Forall Exists* Queries,” MPI-I-2009-RG1-001, 2009.
  9. Report
    RG1
    “Superposition for Fixed Domains,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-2009-RG1-005, 2009.
  10. Report
    RG1
    “Decidability Results for Saturation-based Model Building,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-2009-RG1-004, 2009.
  11. Conference paper
    RG1
    “System Description: H-PILoT,” in Automated Deduction - CADE-22, Montreal, Canada, 2009.
  12. Conference paper
    RG1
    “Incremental Instance Generation in Local Reasoning,” in Computer Aided Verification (CAV 2009), Grenoble, France, 2009.
  13. Conference paper
    RG1
    “Analysis of Authorizations in SAP R/3,” in Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP’09), Oslo, Norway, 2009.
  14. Conference paper
    RG1
    “Analysis of Authorizations in SAP R/3,” in FTP 2009 Workshop Proceedings, 2009.
  15. Article
    RG1
    “Ranking Functions for Size‐change Termination,” ACM Transactions on Programming Languages and Systems, vol. 31, no. 3, 2009.
  16. Proceedings
    RG1
    Eds., Joint proceedings of UNIF 2009 (23nd International Workshop on Unification) and ADDCT 2009 (Automated Deduction: Decidability, Complexity, Tractability). -, 2009.
  17. Proceedings
    RG1
    Eds., First-Order Theorem Proving: FTP 2009 Workshop Proceedings. University of Oslo, Department of Informatics, 2009.
  18. Report
    RG1
    “Constraint Solving for Interpolation,” 2009.
  19. Conference paper
    RG1
    “Locality results for certain extensions of theories with bridging functions,” in Automated Deduction - CADE-22, Montreal, Canada, 2009.
  20. Article
    RG1
    “Sheaves and geometric logic and applications to modular verification of complex systems,” Electronic Notes in Theoretical Computer Science, vol. 230, 2009.
  21. Other
    RG1
    “Reasoning in Complex Theories and Applications. Advanced Lecture, ESSLLI 2009.” ESSLLI 2009 CDrom, 2009.
  22. Conference paper
    RG1D5
    “External Sources of Axioms in Automated Theorem Proving,” in KI 2009: Advances in Artificial Intelligence, Paderborn, Germany, 2009.
  23. Conference paper
    RG1
    “SPASS Version 3.5,” in 22nd International Conference on Automated Deduction (CADE-22), 2009.
  24. Report
    RG1
    “Contextual Rewriting,” MPI-I-2009-RG1-002, 2009.

2008

  1. Proceedings
    RG1
    Eds., Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR’08. CEDAR, 2008.
  2. Report
    RG1
    “Labelled splitting,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-2008-RG1-001, 2008.
  3. Conference paper
    RG1
    “Labelled Splitting,” in Automated Reasoning (IJCAR 2008), Sydney, Australia, 2008.
  4. Thesis
    RG1IMPR-CS
    “Superposition and Decision Procedures - Back and Forth,” Universität des Saarlandes, Saarbrücken, 2008.
  5. Conference paper
    RG1
    “Superposition for Fixed Domains,” in Computer Science Logic : 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, 2008.
  6. Conference paper
    RG1
    “On local reasoning in verification,” in Tools and Algorithms for the Construction and Analysis of Systems : 14th International Conference, TACAS 2008 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, 2008.
  7. Conference paper
    RG1
    “Incremental Instance Generation in Local Reasoning,” in Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning – CEDAR’08, 2008.
  8. Thesis
    RG1
    “Superposition Modulo Linear Arithmetic,” Universität des Saarlandes, Saarbrücken, 2008.
  9. Thesis
    RG1
    “Analysis of Authorizations in SAP R/3,” Universität des Saarlandes, Saarbrücken, 2008.
  10. Conference paper
    RG1
    “SMELS: Satisfiability Modulo Equality with Lazy Superposition,” in Automated Technology for Verification and Analysis (ATVA 2008), Seoul, Korea, 2008.
  11. Thesis
    RG1
    “Bitvector Reasoning with SPASS,” Universität des Saarlandes, Saarbrücken, 2008.
  12. Conference paper
    RG1
    “Reasoning in Complex Theories and Applications,” in KI 2008 : Tutorial 2, 2008.
  13. Conference paper
    RG1
    “Efficient hierarchical reasoning about functions over numerical domains,” in KI 2008: Advances in Artificial Intelligence : 31st Annual German Conference on AI, KI 2008, 2008.
  14. Article
    RG1
    “Interpolation in local theory extensions,” Logical Methods in Computer Science, vol. 4, no. 4, 2008.
  15. Report
    RG1
    “Efficient Hierarchical Reasoning about Functions over Numerical Domains,” SFB/TR 14 AVACS, ATR45, 2008.
  16. Conference paper
    RG1
    “Locality and subsumption testing in EL and some of its extensions,” in Proceedings of the 21st International Workshop on Description Logics (DL-2008), 2008.
  17. Conference paper
    RG1
    “Locality and subsumption testing in EL and some of its extensions,” in Advances in Modal Logic 7 : [Proceedings of the AiML 2008], 2008.
  18. Report
    RG1
    “Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems,” SFB/TR 14 AVACS, ATR46, 2008.
  19. Thesis
    IMPR-CSRG1
    “Stability Proofs for Hybrid Systems,” Universität des Saarlandes, Saarbrücken, 2008.
  20. Conference paper
    RG1
    “Contextual Rewriting in SPASS,” in PAAR-2008/ESHOL-2008 : First International Workshop on Practical Aspects of Automated Reasoning, 2008.

2007

  1. Conference paper
    RG1
    “Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space,” in Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, 2007.
  2. Thesis
    RG1
    “First-order Proof Documentation,” Universität des Saarlandes, Saarbrücken, 2007.
  3. Conference paper
    RG1
    “Verifying CSP-OZ-DC specifications with complex data types and timing parameters,” in Integrated Formal Methods : 6th International Conference, IFM 2007, 2007.
  4. Thesis
    RG1
    “Labelled Splitting,” Universität des Saarlandes, Saarbrücken, 2007.
  5. Article
    RG1
    “Model-based User-interface Management for Public Services,” Electronic Journal of e-Government, vol. 5, no. 1, 2007.
  6. Proceedings
    RG1
    Eds., Workshop Automated Deduction: Decidability, Complexity, Tractability (ADDCT’07). n/a, 2007.
  7. Report
    RG1
    “Superposition for Finite Domains,” Max-Planck-Institut für Informatik, Saarbrücken, Germany, MPI-I-2007-RG1-002, 2007.
  8. Article
    RG1
    “Applications of hierarchical reasoning in the verification of complex systems,” Electronic Notes in Theoretical Computer Science, vol. 174, no. 8, 2007.
  9. Article
    RG1
    “Comparing Instance Generation Methods for Automated Reasoning,” Journal of Automated Reasoning, vol. 38, no. 1/3, 2007.
  10. Conference paper
    RG1
    “Labelled Clauses,” in Automated Deduction - CADE-21 : 21st International Conference on Automated Deduction, 2007.
  11. Conference paper
    RG1
    “An Extension of the Knuth-Bendix Ordering with LPO-like Properties,” in Logic for Programming, Artificial Intelligence, and Reasoning : 14th International Conference, LPAR 2007, 2007.
  12. Conference paper
    RG1
    “Automatic Decidability and Combinability Revisited,” in Automated Deduction – CADE-21 : 21st International Conference on Automated Deduction, 2007.
  13. Conference paper
    RG1
    “Combining Proof Producing Decision Procedures,” in Frontiers of Combining Systems : 6th International Symposium, FroCoS 2007, 2007.
  14. Conference paper
    RG1
    “Constraint Solving for Interpolation,” in Verification, Model Checking and Abstract Interpretation : 8th International Conference, VMCAI 2007, 2007.
  15. Article
    RG1
    “Automated reasoning in some local extensions of ordered structures,” Journal of Multiple-Valued Logic and Soft Computing, vol. 13, no. 4–6, 2007.
  16. Conference paper
    RG1
    “Local Theory Extensions, Hierarchical Reasoning and Applications to Verification,” in Deduction and Decision Procedures, 2007.
  17. Book chapter / section
    RG1
    “Algebraic and logical methods in computer science: some aspects,” in Grigore C. Moisil and his followers, Bucharest, Romania: Editura Academiei Romane, 2007.
  18. Conference paper
    RG1
    “Automated reasoning in some local extensions of ordered structures,” in Proceedings of the 37th International Symposium on Multiple-Valued Logic (ISMVL’07), 2007.
  19. Conference paper
    RG1
    “On unification in certain finitely generated varieties of algebras,” in Proceedings of the 21th International Workshop on Unification (UNIF 2007), 2007.
  20. Article
    RG1
    “Automated theorem proving by resolution in non-classical logics,” Annals of Mathematics and Artificial Intelligence, vol. 49, no. 1–4, 2007.
  21. Conference paper
    RG1
    “Hierarchical and modular reasoning in complex theories: The case of local theory extensions,” in Frontiers of Combining Systems : 6th International Symposium, FroCos 2007, 2007.
  22. Article
    RG1
    “On unification for bounded distributive lattices,” ACM Transactions on Computational Logic, vol. 8, no. 2, 2007.
  23. Thesis
    RG1
    “Conception de Procedures de Decision par Combinaison et Saturation,” Université Henri Poincaré, Nancy, 2007.
  24. Conference paper
    RG1
    “System Description: Spass Version 3.0,” in Automated Deduction - CADE-21, Bremen, Germany, 2007.
  25. Thesis
    RG1
    “Contextual Rewriting in SPASS,” Universität des Saarlandes, Saarbrücken, 2007.
  26. Conference paper
    RG1
    “Modelling of Cross-Organizational Business Processes,” in EMISA 2007 : enterprise modelling and information systems architectures ; concepts and architectures, 2007.
  27. Article
    RG1
    “Modelling of Cross-Organizational Business Processes - Current Methods and Standards,” Enterprise Modelling and Information Systems Architectures, vol. 2, no. 2, 2007.
  28. Thesis
    RG1
    “Intelligent Combination of a First Order Theorem Prover and SMT Procedures,” Universität des Saarlandes, Saarbrücken, 2007.

2006

  1. Thesis
    RG1
    “Netflow analysis of SAP R/3 traffic in an enterprise environment,” Universität des Saarlandes, Saarbrücken, 2006.
  2. Thesis
    RG1
    “Maschinell unterstützte Analyse eines Sicherheitsprotokolls,” Universität des Saarlandes, Saarbrücken, 2006.
  3. Conference paper
    RG1
    “Automatic Verification of Hybrid Systems with Large Discrete State Space,” in Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, 2006.
  4. Conference paper
    RG1
    “Model-based user-interface management for public services,” in 6th European Conference on e-Government, 2006.
  5. Article
    RG1
    “Lexecute: Visualisation and representation of legal procedures,” Digital Evidence Journal, vol. 3, no. 1, 2006.
  6. Article
    RG1
    “Modular Proof Systems for Partial Functions with Evans Equality,” Information and Computation, vol. 204, no. 10, 2006.
  7. Conference paper
    RG1
    “Sudokus as Logical Puzzles,” in Disproving’06: Non-Theorems, Non-Validity, Non-Provability, 2006.
  8. Conference paper
    RG1
    “Applications of hierarchical reasoning in the verification of complex systems,” in PDPAR’06: Pragmatical Aspects of Decision Procedures in Automated Reasoning, 2006.
  9. Conference paper
    RG1
    “Approximate Closed-Form Aggregation of a Fork-Join Structure in Generalised Stochastic Petri Nets,” in Proceedings of the 1st International Conference on Performance Evaluation Methodolgies and Tools, VALUETOOLS 2006, 2006.
  10. Conference paper
    RG1
    “SPASS+T,” in Proceedings of the FLoC’06 Workshop on Empirically Successful Computerized Reasoning (ESCoR 2006), Seattle, WA, USA, 2006.
  11. Conference paper
    RG1
    “Using BPEL processes defined by Event-driven Process Chains,” in 5. GI-Workshop “EPK 2006 - Geschäftsprozessmanagement mit Ereignisgesteuerten Prozessketten,” 2006.
  12. Conference paper
    RG1
    “Interpolation in local theory extensions,” in Proceedings of IJCAR 2006, 2006.
  13. Article
    RG1
    “Automatisches Beweisen in komplexen Theorien,” Jahrbuch der Max-Planck-Gesellschaft, vol. -, 2006.
  14. Conference paper
    RG1
    “Sheaves and geometric logic in concurrency,” in Proceedings of the Eighth Workshop on Geometric and Topological Methods in Concurrency (GETCO 2006), 2006.
  15. Conference paper
    RG1
    “Local reasoning in verification,” in IJCAR’06 Workshop : VERIFY'06: Verification Workshop, 2006.

2005

  1. Conference paper
    RG1
    “On the semantics of EPCs: Faster calculation for EPCs with small state spaces,” in EPK 2005. 4. Workshop der GI, Arbeitskreis: Geschäftsprozessmanagement mit Ereignisgesteuerten Prozessketten, 2005.
  2. Conference paper
    RG1
    “Integration of a Software Model Checker into Isabelle,” in Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005, 2005.
  3. Conference paper
    RG1
    “Enhanced Workflow Models as a Tool for Judicial Practitioners,” in On the move to meaningful internet systems 2005: OTM 2005 Workshops : OTM Confederated International Workshops and Posters, AWeSOMe, CAMS, GADA, MIOS+INTEROP, ORM, PhDS, SeBGIS, SWWS, and WOSE 2005, 2005.
  4. Conference paper
    RG1
    “Comparing Instance Generation Methods for Automated Reasoning,” in Automated Reasoning with Analytic Tableaux and Related Methods : International Conference, TABLEAUX 2005, 2005.
  5. Article
    D1RG1
    “Harald Ganzinger : 31.10.1950 - 3.6.2004,” Jahrbuch der Max-Planck-Gesellschaft, 2005.
  6. Conference paper
    RG1
    “Hierarchic reasoning in local theory extensions,” in Automated deduction - CADE-20 : 20th International Conference on Automated Deduction, 2005.
  7. Conference paper
    RG1
    “An Abstract Model of Routing in Mobile Ad Hoc Networks,” in Sixth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, 2005.

2004

  1. Conference paper
    RG1
    “Darwin: A Theorem Prover for the Model Evolution Calculus,” in Proceedings of the 1st Workshop on Empirically Successful First Order Reasoning (ESFOR’04), 2004.
  2. Conference paper
    RG1
    “Modular Proof Systems for Partial Functions with Weak Equality,” in Automated reasoning : Second International Joint Conference, IJCAR 2004, 2004.
  3. Conference paper
    IMPR-CSRG1
    “A Superposition View on Nelson-Oppen,” in Contributions to the Doctoral Programme of the 2nd International Joint Conference on Automated Reasoning, 2004.
  4. Thesis
    RG1
    “Instance Generation Methods for Automated Reasoning,” Universität des Saarlandes, Saarbrücken, Saarland, 2004.
  5. Conference paper
    RG1
    “Resolution-based decision procedures for the positive theory of some finitely generated varieties of algebras,” in Proceedings of the 34th International Symposium on Multiple-Valued Logic (ISMVL-2004), 2004.

2003

  1. Article
    IMPR-CSRG1
    “On Using Ground Joinable Equations in Equational Theorem Proving,” Journal of Symbolic Computation, vol. 36, 2003.
  2. Conference paper
    IMPR-CSRG1
    “The New WALDMEISTER Loop at Work,” in Automated deduction, CADE-19 : 19th International Conference on Automated Deduction, Miami, Florida, 2003.
  3. Conference paper
    IMPR-CSRG1
    “Superposition modulo a Shostak Theory,” in Automated Deduction, CADE-19 : 19th International Conference on Automated Deduction, Miami, Florida, 2003.
  4. Conference paper
    IMPR-CSRG1
    “Citius altius fortius: Lessons learned from the Theorem Prover WALDMEISTER,” in Proceedings of the 4th International Workshop on First Order Theorem Proving, FTP’03, Valencia, Spain, 2003.
  5. Book chapter / section
    RG1
    “Representation Theorems and the Semantics of Non-classical Logics, and Applications to Automated Theorem Proving,” in Beyond Two: Theory and Applications of Multiple Valued Logic, vol. 114, M. Fitting and E. Orlowska, Eds. Berlin, Germany: Springer, 2003.
  6. Conference paper
    RG1
    “Automated theorem proving by resolution in non-classical logics,” in Fourth International Conference Journees de l’Informatique Messine: Knowledge Discovery and Discrete Mathematics (JIM-03), Metz, France, 2003.
  7. Article
    RG1
    “Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators,” Journal of Symbolic Computation, vol. 36, 2003.

2002

  1. Conference paper
    IMPR-CSRG1
    “The Next WALDMEISTER Loop,” in Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, Copenhagen, Denmark, 2002.
  2. Conference paper
    IMPR-CSRG1
    “Is Logic Effective for Analyzing C Programs?,” in Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi, Saarbrücken, 2002.
  3. Article
    IMPR-CSRG1
    “A Phytography of WALDMEISTER,” AI Communications, vol. 15, 2002.
  4. Conference paper
    RG1
    “On uniform word problems involving bridging operators on distributive lattices,” in Automated Reasoning with Analytic and Related Methods : International Conference, TABLEAUX 2002, Copenhagen, Denmark, 2002.
  5. Article
    RG1
    “Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part I),” Journal of Symbolic Computation, vol. 33, 2002.
  6. Article
    RG1
    “Cancellative Abelian Monoids and Related Structures in Refutational Theorem Proving (Part II),” Journal of Symbolic Computation, vol. 33, 2002.
  7. Conference paper
    RG1
    “A New Input Technique for Accented Letters in Alphabetical Scripts,” in Proceedings of the 20th International Unicode Conference, Washington, DC, USA, 2002.
  8. Conference paper
    RG1IMPR-CSD4
    “SPASS Version 2.0,” in Automated deduction, CADE-18 : 18th International Conference on Automated Deduction, Kopenhagen, Denmark, 2002.

2001

  1. Conference paper
    IMPR-CSRG1
    “First-Order Atom Definitions Extended,” in Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-2001), 2001.
  2. Conference paper
    RG1
    “The Next WALDMEISTER Loop (Extended Abstract),” in Proceedings of the Second International Workshop on the Implementation of Logics, IWIL 2001, 2001.
  3. Conference paper
    IMPR-CSRG1
    “On the Evaluation of Indexing Techniques for Theorem Proving,” in Automated reasoning : First International Joint Conference, IJCAR 2001, 2001.
  4. Book chapter / section
    RG1
    “Computing small clause normal forms,” in Handbook of Automated Reasoning, vol. 1, Amsterdam: Elsevier, 2001.
  5. Report
    RG1
    “Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-2001-2-005, 2001.
  6. Report
    RG1
    “Superposition and chaining for totally ordered divisible abelian groups,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-2001-2-001, 2001.
  7. Conference paper
    RG1
    “Superposition and Chaining for Totally Ordered Divisible Abelian Groups (Extended Abstract),” in Automated reasoning : First International Joint Conference, IJCAR 2001, 2001.
  8. Book chapter / section
    RG1
    “Combining Superposition, Sorts and Splitting,” in Handbook of Automated Reasoning, vol. 1, Amsterdam: Elsevier, 2001.

2000

  1. Conference paper
    RG1
    “Chaining Techniques for Automated Theorem Proving in Many-Valued Logics,” in Proceedings of the 30th IEEE International Symposium on Multiple-Valued Logic (ISMVL-00), 2000.
  2. Book chapter / section
    RG1
    “SHn-algebras (Symmetric Heyting algebras of order n),” in COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, Tampere: Tampere University of Technology (Mathematics), 2000.
  3. Conference paper
    RG1
    “On unification for bounded distributive lattices,” in Proceedings of the 17th International Conference on Automated Deduction (CADE-17), 2000.
  4. Article
    RG1
    “Duality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. Part II,” Studia Logica, vol. 64, no. 2, 2000.
  5. Book chapter / section
    RG1
    “Some properties of Kleene algebras,” in COST Action 15 (Many-Valued Logics for Computer Science Applications) ATLAS of Many-Valued Structures, Tampere: Tampere University of Technology (Mathematics), 2000.
  6. Article
    RG1
    “Duality and Canonical Extensions of Bounded Distributive Lattices with Operators and Applications to the Semantics of Non-Classical Logics. Part I,” Studia Logica, vol. 64, no. 1, 2000.
  7. Conference paper
    RG1
    “Resolution-based theorem proving for SHn-logics,” in Automated Deduction in Classical and Non-Classical Logic (Selected Papers of FTP’98), 2000.
  8. Article
    RG1
    “Priestley Duality for SHn-algebras and Applications to the Study of Kripke-style Models for SHn-logics,” Multiple-Valued Logic - an International Journal, vol. 5, no. 4, 2000.
  9. Thesis
    RG1
    “Entscheidbarkeitsprobleme für monadische (Horn)Klauselklassen,” Universität des Saarlandes, Naturwissenschaftlich-Technische Fakultät, Saarbrücken, 2000.

1999

  1. Conference paper
    RG1
    “On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results,” in Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 1999.
  2. Conference paper
    RG1
    “Priestley representation for distributive lattices with operators and applications to automated theorem proving,” in Dualities, Interpretability and Ordered Structures, 1999.
  3. Conference paper
    RG1
    “Modeling Interaction by Sheaves and Geometric Logic,” in Proceedings of the 12th International Symposium Fundamentals of Computation Theory (FCT-99), 1999.
  4. Conference paper
    RG1
    “Representation Theorems and Automated Theorem Proving in Non-Classical Logics,” in Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic (ISMVL-99), 1999.
  5. Conference paper
    RG1
    “Resolution-based Theorem Proving for Non-classical Logics based on Distributive Lattices with Operators,” in Volume of Abstracts / 11th International Congress of Logic, Methodology and Philosophy of Science, Cracow, Poland, 1999.
  6. Conference paper
    RG1
    “Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups,” in Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR-99), 1999.
  7. Report
    RG1
    “Cancellative superposition decides the theory of divisible torsion-free abelian groups,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-1999-2-003, 1999.
  8. Article
    RG1
    “SPASS V0.95TPTP,” Journal of Automated Reasoning, vol. 23, no. 1, 1999.
  9. Conference paper
    RG1D4
    “System Description: SPASS Version 1.0.0,” in Automated deduction (CADE-16) : 16th international conference on automated deduction, 1999.
  10. Conference paper
    RG1
    “Towards an Automatic Analysis of Security Protocols in First-Order Logic,” in Proceedings of the 16th International Conference on Automated Deduction (CADE-16), 1999.

1998

  1. Conference paper
    RG1
    “Optimised Functional Translation and Resolution,” in Proceedings of the International Conference on Automated Reaso ning with Analytic Tableaux and Related Methods (TABLEAUX’98), 1998.
  2. Conference paper
    RG1
    “Unification in Extensions of Shallow Equational Theories,” in Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98), 1998.
  3. Article
    RG1
    “Paradigmen und Perspektiven der automatischen Deduktion,” KI, Organ des Fachbereichs 1 "Künstliche Intelligenz’' der Gesellschaft für Informatik e.V., vol. 4, 1998.
  4. Conference paper
    RG1
    “On Generating Small Clause Normal Forms,” in Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 1998.
  5. Report
    RG1
    “Resolution-based Theorem Proving for SHn-Logics,” Technische Universität Wien, Vienna, Austria, E1852-GS-981, 1998.
  6. Conference paper
    RG1
    “On Translation of Finitely-Valued Logics to Classical First-Order Logic,” in Proceedings of the 13th European Conference on Artificial Intelligence (ECAI-98), 1998.
  7. Conference paper
    RG1
    “Representation Theorems and Automated Theorem Proving in Certain Classes of Non-classical Logics,” in Proceedings of the Workshop on Many-Valued Logic for AI Applications (ECAI 1998), Brighton, UK, 1998.
  8. Article
    RG1
    “Extending reduction orderings to ACU-compatible reduction orderings,” Information Processing Letters, vol. 67, no. 1, 1998.
  9. Conference paper
    RG1
    “Superposition for Divisible Torsion-Free Abelian Groups,” in Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 1998.
  10. Article
    RG1
    “SPASS V0.77,” Journal of Automated Reasoning, vol. 21, no. 1, 1998.
  11. Book chapter / section
    RG1
    “Rechnen in sortierter Prädikatenlogik,” in Ausgezeichnete Informatikdissertationen 1997, Stuttgart, Germany: Teubner, 1998.
  12. Book chapter / section
    RG1
    “Sorted Unification and Tree Automata,” in Automated Deduction - A Basis for Applications, Dordrecht, The Netherlands: Kluwer, 1998.

1997

  1. Conference paper
    RG1
    “Soft Typing for Ordered Resolution,” in Automated Deduction - CADE-14, Townsville, Australia, 1997.
  2. Conference paper
    RG1
    “A Superposition Calculus for Divisible Torsion-Free Abelian Groups,” in Proceedings of the International Workshop on First-Order Theorem Proving (FTP-97), 1997.
  3. Thesis
    RG1
    “Cancellative Abelian Monoids in Refutational Theorem Proving,” Universität des Saarlandes, Saarbrücken, 1997.
  4. Article
    RG1
    “SPASS Version 0.49,” Journal of Automated Reasoning, vol. 18, no. 2, 1997.

1996

  1. Conference paper
    RG1
    “Theorem Proving in Cancellative Abelian Monoids (Extended Abstract),” in Automated Deduction - CADE-13, New Brunswick, USA, 1996.
  2. Report
    RG1
    “Common Syntax of the DFG-Schwerpunktprogramm Deduktion’',” Universität Karlsruhe, Karlsruhe, 10/96, 1996.
  3. Conference paper
    RG1
    “Sorted Unification and Its Application to Automated Theorem Proving,” in Proceedings of the CADE-13 Workshop: Term Schematizations and Their Applications, 1996.
  4. Conference paper
    RG1
    “SPASS & FLOTTER, Version 0.42,” in Automated Deduction - CADE-13, New Brunswick, NJ, USA, 1996.
  5. Conference paper
    RG1
    “Unification in Sort Theories,” in Proceedings of the 10th International Workshop on Unification, UNIF’96, 1996.
  6. Article
    RG1
    “Unification in Sort Theories and its Applications,” Annals of Mathematics and Artificial Intelligence, vol. 18, no. 2/4, 1996.
  7. Thesis
    RG1
    “Computational Aspects of a First-Order Logic with Sorts,” Universität des Saarlandes, Saarbrücken, 1996.
  8. Conference paper
    RG1
    “Unification in Pseudo-Linear Sort Theories is Decidable,” in Proceedings of the 13th International Conference on Automated Deduction (CADE-13), New Brunswick, USA, 1996.

1995

  1. Article
    RG1
    “Basic Paramodulation,” Information and Computation, vol. 121, no. 2, 1995.
  2. Conference paper
    RG1
    “Workshop CPL Computational Propositional Logic,” in KI-95 Activities: Workshops, Posters, Demos, Bielefeld, Germany, 1995.
  3. Article
    RG1
    “A Note on Assumptions about Skolem Functions,” Journal of Automated Reasoning, vol. 15, no. 2, 1995.
  4. Article
    RG1
    “First-Order Tableaux with Sorts,” Logic Journal of the IGPL, vol. 3, no. 6, 1995.

1994

  1. Article
    RG1
    “Refutational Theorem Proving for Hierarchic First-Order Theories,” Applicable Algebra in Engineering, Communication and Computing (AAECC), vol. 5, no. 3/4, 1994.
  2. Conference paper
    RG1
    “Description Logics for Natural Language Processing,” in International Workshop on Description Logics (DL 1994), Bonn, Germany, 1994.
  3. Conference paper
    RG1
    “First-Order Tableaux with Sorts,” in TABLEAUX-’94, 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 1994.

1993

  1. Conference paper
    RG1
    “Set Constraints are the Monadic Class,” in Eighth Annual IEEE Symposium on Logic in Computer Science, Montreal, Canada, 1993.
  2. Conference paper
    RG1
    “Superposition with simplification as a decision procedure for the monadic class with equality,” in Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC’93, Brno, Czech Republic, 1993.
  3. Report
    RG1
    “Basic paramodulation,” Max-Planck-Institut für Informatik, Saarbrücken, MPI-I-93-236, 1993.
  4. Conference paper
    RG1
    “Extending the Resolution Method with Sorts,” in Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI ’93), Chambéry, France, 1993, vol. 1.
  5. Conference paper
    RG1
    “A New Sorted Logic,” in GWAI-92: Advances in Artificial Inteligence, Bonn, 1993.

1992

  1. Conference paper
    RG1
    “Basic Paramodulation and Superposition,” in Automated Deduction - CADE-11, Saratoga Springs, NY, 1992.
  2. Conference paper
    RG1
    “Termination Proofs of Well-Moded Logic Programs Via Conditional Rewrite Systems,” in Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems ’92 (CTRS 1992), Pont-à-Mousson, France, 1992.
  3. Article
    RG1
    “Semantics of Order-Sorted Specifications,” Theoretical Computer Science, vol. 94, no. 1, 1992.

1990

  1. Conference paper
    RG1
    “A Resolution Calculus with Dynamic Sort Structures and Partial Functions,” in Proceedings of the 9th European Conference on Artificial Intelligence (ECAI 1990), Stockholm Sweden, 1990.