HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

On the Word, Subsumption, and Complement Problem for Recurrent Term Schematizations

Miki Hermann 1 Gernot Salzer
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We investigate the word and the subsumption problem for recurrent term schematizations, which are a special type of constraints based on iteration. By means of unification, we reduce these problems to a fragment of Presburger arithmetic. Our approach is applicable to all recurrent term schematizations having a finitary unification algorithm. Furthermore, we study a particular form of the complement problem. Given a finite set of terms, we ask whether its complement can be finitely represented by schematizations, using only the equality predicate without negation. The answer is negative as there are ground terms too complex to be represented by schematizations with limited resources.
Document type :
Conference papers
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:16:32 AM
Last modification on : Friday, February 4, 2022 - 3:31:02 AM
Long-term archiving on: : Wednesday, March 29, 2017 - 12:37:30 PM


  • HAL Id : inria-00098687, version 1



Miki Hermann, Gernot Salzer. On the Word, Subsumption, and Complement Problem for Recurrent Term Schematizations. 23nd International Conference on Mathematical Foundations of Computer Science, 1998, Brno, République Tchèque, pp.257-266. ⟨inria-00098687⟩



Record views


Files downloads