Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-540-85958-1_33
Title: A coinduction rule for entailment of recursively defined properties
Authors: Jaffar, J. 
Santosa, A.E. 
Voicu, R. 
Issue Date: 2008
Source: Jaffar, J.,Santosa, A.E.,Voicu, R. (2008). A coinduction rule for entailment of recursively defined properties. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5202 LNCS : 493-508. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-540-85958-1_33
Abstract: Recursively defined properties are ubiquitous. We present a proof method for establishing entailment of such properties and over a set of common variables. The main contribution is a particular proof rule based intuitively upon the concept of coinduction. This rule allows the inductive step of assuming that an entailment holds during the proof the entailment. In general, the proof method is based on an unfolding (and no folding) algorithm that reduces recursive definitions to a point where only constraint solving is necessary. The constraint-based proof obligation is then discharged with available solvers. The algorithm executes the proof by a search-based method which automatically discovers the opportunity of applying induction instead of the user having to specify some induction schema, and which does not require any base case. © 2008 Springer-Verlag Berlin Heidelberg.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/41110
ISBN: 3540859578
ISSN: 03029743
DOI: 10.1007/978-3-540-85958-1_33
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

3
checked on Jan 17, 2018

Page view(s)

45
checked on Jan 14, 2018

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.