Publication | Date of Publication | Type |
---|
Interpolation Results for Arrays with Length and MaxDiff | 2023-11-03 | Paper |
Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties | 2023-08-26 | Paper |
https://portal.mardi4nfdi.de/entity/Q6159930 | 2023-06-23 | Paper |
Existence and Construction of a Gr\"obner Basis for a Polynomial Ideal | 2023-06-15 | Paper |
Consider only general superpositions in completion procedures | 2022-12-09 | Paper |
Deciding the word problem for ground identities with commutative and extensional symbols | 2022-11-09 | Paper |
Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols | 2022-10-24 | Paper |
Automated reasoning about parallel algorithms using powerlists | 2022-08-16 | Paper |
https://portal.mardi4nfdi.de/entity/Q5094130 | 2022-08-02 | Paper |
Interpolation and amalgamation for arrays with MaxDiff | 2021-10-18 | Paper |
Algorithms for computing greatest common divisors of parametric multivariate polynomials | 2020-09-19 | Paper |
An Efficient Algorithm for Computing Parametric Multivariate Polynomial GCD | 2020-09-09 | Paper |
Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation | 2020-08-05 | Paper |
NIL: learning nonlinear interpolants | 2020-03-10 | Paper |
Conditional congruence closure over uninterpreted and interpreted symbols | 2019-03-06 | Paper |
Lemma discovery in automating induction | 2019-01-15 | Paper |
The Generalized Rabinowitsch Trick | 2018-04-05 | Paper |
Shostak's congruence closure as completion | 2017-11-17 | Paper |
A total, ground path ordering for proving termination of AC-rewrite systems | 2017-11-17 | Paper |
Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm | 2017-09-06 | Paper |
Unification and Matching in Hierarchical Combinations of Syntactic Theories | 2017-02-27 | Paper |
Conditions for determinantal formula for resultant of a polynomial system | 2017-02-03 | Paper |
Maximal extensions of simplification orderings | 2017-01-19 | Paper |
https://portal.mardi4nfdi.de/entity/Q2819403 | 2016-09-29 | Paper |
An Algorithm to Check Whether a Basis of a Parametric Polynomial System is a Comprehensive Gröbner Basis and the Associated Completion Algorithm | 2016-09-29 | Paper |
Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF | 2016-09-05 | Paper |
Conditions for exact resultants using the Dixon formulation | 2015-11-26 | Paper |
A new algorithm for computing comprehensive Gröbner systems | 2015-09-17 | Paper |
When Is a Formula a Loop Invariant? | 2015-09-14 | Paper |
Computing comprehensive Gröbner systems and comprehensive Gröbner bases simultaneously | 2015-06-09 | Paper |
Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures | 2014-07-22 | Paper |
On Asymmetric Unification and the Combination Problem in Disjoint Theories | 2014-04-16 | Paper |
On invariant checking | 2014-01-27 | Paper |
Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants | 2013-08-16 | Paper |
Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis | 2013-06-14 | Paper |
Hierarchical Combination | 2013-06-14 | Paper |
Harald Ganzinger’s Legacy: Contributions to Logics and Programming | 2013-04-19 | Paper |
Elimination Techniques for Program Analysis | 2013-04-19 | Paper |
Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants | 2013-04-16 | Paper |
An efficient method for computing comprehensive Gröbner bases | 2013-03-11 | Paper |
An efficient algorithm for computing a comprehensive Gröbner system of a parametric polynomial system | 2013-01-10 | Paper |
A “Hybrid” Approach for Synthesizing Optimal Controllers of Hybrid Systems: A Case Study of the Oil Pump Industrial Example | 2012-11-08 | Paper |
Rewriting Induction + Linear Arithmetic = Decision Procedure | 2012-09-05 | Paper |
Program Analysis Using Quantifier-Elimination Heuristics | 2012-07-16 | Paper |
A brief introduction to Wen-Tsun Wu's Academic career | 2012-05-07 | Paper |
Termination Analysis of C Programs Using Compiler Intermediate Languages | 2012-04-24 | Paper |
Multivariate Resultants in Bernstein Basis | 2011-05-26 | Paper |
An algorithm for computing a Gröbner basis of a polynomial ideal over a ring with zero divisors | 2011-02-19 | Paper |
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study | 2010-09-14 | Paper |
Predicting Failures of and Repairing Inductive Proof Attempts | 2010-06-02 | Paper |
Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions | 2010-05-07 | Paper |
Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures | 2010-04-27 | Paper |
Automated Deduction – CADE-19 | 2010-04-20 | Paper |
Shape Analysis with Reference Set Relations | 2010-01-14 | Paper |
Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation | 2009-08-11 | Paper |
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs | 2009-07-28 | Paper |
Cayley-Dixon projection operator for multi-univariate composed polynomials | 2009-06-11 | Paper |
Dependency Pairs for Rewriting with Non-free Constructors | 2009-03-06 | Paper |
Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures | 2008-08-28 | Paper |
Inductive Decidability Using Implicit Induction | 2008-05-27 | Paper |
Bruno Buchberger -- a life devoted to symbolic computation (Preface to the special issue) | 2007-10-23 | Paper |
Generating all polynomial invariants in simple loops | 2007-10-23 | Paper |
Constructing Sylvester-type resultant matrices using the Dixon formulation | 2007-08-24 | Paper |
Resultants for unmixed bivariate polynomial systems produced using the Dixon formulation | 2007-08-24 | Paper |
A quantifier-elimination based heuristic for automatically generating inductive assertions for programs | 2007-05-24 | Paper |
Automatic generation of polynomial invariants of bounded degree using abstract interpretation | 2007-01-22 | Paper |
Computer Algebra in Scientific Computing | 2006-07-07 | Paper |
Obituary: Harald Ganzinger | 2006-01-16 | Paper |
Mechanizing Mathematical Reasoning | 2006-01-10 | Paper |
Theoretical Aspects of Computing - ICTAC 2004 | 2005-11-30 | Paper |
Static Analysis | 2005-08-24 | Paper |
https://portal.mardi4nfdi.de/entity/Q3021913 | 2005-06-21 | Paper |
https://portal.mardi4nfdi.de/entity/Q4660683 | 2005-04-04 | Paper |
https://portal.mardi4nfdi.de/entity/Q4657307 | 2005-03-14 | Paper |
Automatic Generation of Polynomial Loop Invariants | 2005-03-14 | Paper |
Exact resultants for corner-cut unmixed multivariate polynomial systems using the Dixon formulation | 2004-08-20 | Paper |
https://portal.mardi4nfdi.de/entity/Q4737127 | 2004-08-11 | Paper |
https://portal.mardi4nfdi.de/entity/Q4470525 | 2004-07-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q4447232 | 2004-02-16 | Paper |
https://portal.mardi4nfdi.de/entity/Q4539635 | 2002-07-10 | Paper |
https://portal.mardi4nfdi.de/entity/Q2751760 | 2002-04-11 | Paper |
https://portal.mardi4nfdi.de/entity/Q2778873 | 2002-03-21 | Paper |
https://portal.mardi4nfdi.de/entity/Q2738486 | 2002-03-13 | Paper |
https://portal.mardi4nfdi.de/entity/Q2751759 | 2002-02-27 | Paper |
https://portal.mardi4nfdi.de/entity/Q4234291 | 2001-07-16 | Paper |
https://portal.mardi4nfdi.de/entity/Q2723430 | 2001-07-05 | Paper |
https://portal.mardi4nfdi.de/entity/Q4503901 | 2000-09-14 | Paper |
Using an induction prover for verifying arithmetic circuits | 2000-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q4226953 | 1999-07-14 | Paper |
https://portal.mardi4nfdi.de/entity/Q4227295 | 1999-07-06 | Paper |
https://portal.mardi4nfdi.de/entity/Q4228470 | 1999-06-21 | Paper |
Transformational methodology for proving termination of logic programs | 1998-11-05 | Paper |
https://portal.mardi4nfdi.de/entity/Q3838770 | 1998-08-13 | Paper |
Solving Polynomial Systems Using a Branch and Prune Approach | 1997-11-02 | Paper |
New uses of linear arithmetic in automated theorem proving by induction | 1996-11-04 | Paper |
A path ordering for proving termination of AC rewrite systems | 1995-05-30 | Paper |
Complexity of unification problems with associative-commutative operators | 1993-12-20 | Paper |
https://portal.mardi4nfdi.de/entity/Q4202945 | 1993-09-06 | Paper |
https://portal.mardi4nfdi.de/entity/Q3976057 | 1992-06-26 | Paper |
Automating inductionless induction using test sets | 1991-01-01 | Paper |
Semi-unification | 1991-01-01 | Paper |
Sufficient-completeness, ground-reducibility and their complexity | 1991-01-01 | Paper |
On ground-confluence of term rewriting systems | 1990-01-01 | Paper |
Inference rules and proof procedures for inequations | 1990-01-01 | Paper |
Unnecessary inferences in associative-commutative completion procedures | 1990-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3033866 | 1989-01-01 | Paper |
Computability and implementability issues in abstract data types | 1988-01-01 | Paper |
Only prime superpositions need be considered in the Knuth-Bendix completion procedure | 1988-01-01 | Paper |
Problem corner: Proving equivalence of different axiomatizations of free groups | 1988-01-01 | Paper |
Computing a Gröbner basis of a polynomial ideal over a Euclidean domain | 1988-01-01 | Paper |
Wu's method and its application to perspective viewing | 1988-01-01 | Paper |
A multi-level geometric reasoning system for vision | 1988-01-01 | Paper |
A refutational approach to geometry theorem proving | 1988-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3789100 | 1988-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3805961 | 1988-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3819992 | 1988-01-01 | Paper |
On sufficient-completeness and related properties of term rewriting systems | 1987-01-01 | Paper |
Proof by consistency | 1987-01-01 | Paper |
Complexity of matching problems | 1987-01-01 | Paper |
Matching, unification and complexity | 1987-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3774998 | 1987-01-01 | Paper |
Using Gröbner bases to reason about geometry problems | 1986-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3761697 | 1986-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3783519 | 1986-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3785940 | 1986-01-01 | Paper |
An \(O(| T| ^ 3)\) algorithm for testing the Church-Rosser property of Thue systems | 1985-01-01 | Paper |
Worst-case choice for the stable marriage problem | 1985-01-01 | Paper |
The Church-Rosser property and special Thue systems | 1985-01-01 | Paper |
A finite Thue system with decidable word problem and without equivalent finite canonical system | 1985-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3683533 | 1985-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3685174 | 1985-01-01 | Paper |
The Knuth-Bendix Completion Procedure and Thue Systems | 1985-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3696522 | 1985-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3703293 | 1985-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3677849 | 1984-01-01 | Paper |
On Proving Uniform Termination and Restricted Termination of Rewriting Systems | 1983-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3319767 | 1983-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3687693 | 1982-01-01 | Paper |
https://portal.mardi4nfdi.de/entity/Q3942387 | 1982-01-01 | Paper |