Computer Science – Logic in Computer Science
Scientific paper
2008-11-28
Computer Science
Logic in Computer Science
This is the long version of a paper which appeared in IJCAR 2008. 38 pages
Scientific paper
We propose a procedure for automated implicit inductive theorem proving for equational specifications made of rewrite rules with conditions and constraints. The constraints are interpreted over constructor terms (representing data values), and may express syntactic equality, disequality, ordering and also membership in a fixed tree language. Constrained equational axioms between constructor terms are supported and can be used in order to specify complex data structures like sets, sorted lists, trees, powerlists... Our procedure is based on tree grammars with constraints, a formalism which can describe exactly the initial model of the given specification (when it is sufficiently complete and terminating). They are used in the inductive proofs first as an induction scheme for the generation of subgoals at induction steps, second for checking validity and redundancy criteria by reduction to an emptiness problem, and third for defining and solving membership constraints. We show that the procedure is sound and refutationally complete. It generalizes former test set induction techniques and yields natural proofs for several non-trivial examples presented in the paper, these examples are difficult to specify and carry on automatically with related induction procedures.
Bouhoula Adel
Jacquemard Florent
No associations
LandOfFree
Automated Induction for Complex Data Structures does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Automated Induction for Complex Data Structures, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automated Induction for Complex Data Structures will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-710358