| Publication | Date of Publication | Type |
|---|
AC-complete unification and its application to theorem proving
Rewriting Techniques and Applications | 2022-12-09 | Paper |
“Syntactic” AC-unification
Constraints in Computational Logics | 2022-08-16 | Paper |
A partial solution for \(D\)-unification based on a reduction to AC1-unification
Automata, Languages and Programming | 2019-03-29 | Paper |
| Certifying standard and stratified Datalog inference engines in SSReflect | 2018-01-04 | Paper |
Rewrite systems for natural, integral, and rational arithmetic
Rewriting Techniques and Applications | 2017-11-17 | Paper |
A Coq formalization of the relational data model
Programming Languages and Systems | 2014-04-16 | Paper |
\textsf{CC(X)}: semantic combination of congruence closure with solvable theories
Electronic Notes in Theoretical Computer Science | 2013-12-06 | Paper |
Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation
Logical Methods in Computer Science | 2012-09-25 | Paper |
A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic
Automated Reasoning | 2012-09-05 | Paper |
| Automated certified proofs with CiME3 | 2012-04-24 | Paper |
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
Tools and Algorithms for the Construction and Analysis of Systems | 2011-05-19 | Paper |
Rewriting Techniques and Applications
Lecture Notes in Computer Science | 2009-04-30 | Paper |
Modeling Permutations in Coq for Coccinelle
Rewriting, Computation and Proof | 2009-03-06 | Paper |
Certification of Automated Termination Proofs
Frontiers of Combining Systems | 2008-09-16 | Paper |
Mechanically proving termination using polynomial interpretations
Journal of Automated Reasoning | 2006-11-17 | Paper |
Automated Deduction – CADE-20
Lecture Notes in Computer Science | 2006-11-01 | Paper |
| scientific article; zbMATH DE number 1722699 (Why is no real title available?) | 2002-03-21 | Paper |
| scientific article; zbMATH DE number 1615231 (Why is no real title available?) | 2001-07-08 | Paper |
| scientific article; zbMATH DE number 1303340 (Why is no real title available?) | 1999-11-07 | Paper |
| scientific article; zbMATH DE number 1300966 (Why is no real title available?) | 1999-07-29 | Paper |
Avoiding slack variables in the solving of linear diophantine equations and inequations
Theoretical Computer Science | 1998-07-23 | Paper |
Introducing global constraints in CHIP
Mathematical and Computer Modelling | 1995-04-20 | Paper |
An efficient incremental algorithm for solving systems of linear diophantine equations
Information and Computation | 1995-04-02 | Paper |
Solving \(*\)-problems modulo distributivity by a reduction to \(AC1\)- unification
Journal of Symbolic Computation | 1994-05-05 | Paper |
| scientific article; zbMATH DE number 4213327 (Why is no real title available?) | 1991-01-01 | Paper |
