Name
Abstract | ||
|---|---|---|
Recursively defined properties are ubiquitous. We present a proof method for establishing entailment $\mathcal{G} \models \mathcal{H}$ of such properties $\mathcal{G}$ and $\mathcal{H}$ 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. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-85958-1_33 | CP |
Keywords | Field | DocType |
main contribution,coinduction rule,base case,common variable,constraint-based proof obligation,recursively defined properties,search-based method,particular proof rule,proof method,induction schema,inductive step,available solvers,rule based | Logic program,Discrete mathematics,Logical consequence,Rule-based system,Computer science,Constraint satisfaction problem,Logic programming,Proof obligation,Recursion | Conference |
Volume | ISSN | Citations |
5202 | 0302-9743 | 4 |
PageRank | References | Authors |
0.43 | 20 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Joxan Jaffar | 1 | 2350 | 283.50 |
| Andrew Santosa | 2 | 146 | 13.36 |
| Răzvan Voicu | 3 | 19 | 2.44 |